1 /-
2 Copyright (c) 2017 Mario Carneiro. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Mario Carneiro
5 -/
6 import data.int.basic algebra.associated data.nat.gcd
src └────────────┘ └────────────────┘ └──────────┘
7
8 /-- The ring of integers adjoined with a square root of `d`.
9 These have the form `a + b √d` where `a b : ℤ`. The components
10 are called `re` and `im` by analogy to the negative `d` case,
11 but of course both parts are real here since `d` is nonnegative. -/
12 structure zsqrtd (d : ℤ) := mk {} ::
id ┴
src ┴
typ ┴
13 (re : ℤ)
id ┴
src ┴
typ ┴
14 (im : ℤ)
id ┴
src ┴
typ ┴
15
16 prefix `ℤ√`:100 := zsqrtd
id └────┘
src └────┘
typ └────┘
doc └────┘
17
18 namespace zsqrtd
19 section
20 parameters {d : ℤ}
id ┴
src ┴
typ ┴
21
22 instance : decidable_eq ℤ√d :=
id └──────────┘ └┘┴
src └──────────┘ └┘
typ └──────────┘ └┘┴
doc └┘
23 by tactic.mk_dec_eq_instance
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
par └───────────────────────┘
st └────────────────────────┘
24
25 theorem ext : ∀ {z w : ℤ√d}, z = w ↔ z.re = w.re ∧ z.im = w.im
id ┴ └┘┴ ┴ ┴ ┴ ┴ ┴└─┘ ┴ ┴└─┘ ┴ ┴└─┘ ┴ ┴└─┘
src └┘ ┴ ┴ └─┘ ┴ └─┘ ┴ └─┘ ┴ └─┘
typ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴└─┘ ┴ ┴└─┘ ┴ ┴└─┘ ┴ ┴└─┘
doc └┘
26 | ⟨x, y⟩ ⟨x', y'⟩ := ⟨λ h, by injection h; split; assumption,
id ┴ ┴
src └────────┘ └───┘ └────────┘
typ ┴ └────────┘┴ └───┘ └────────┘
doc └────────┘ └───┘ └────────┘
txt └────────┘ └───┘ └────────┘
par └────────┘ └───┘ └────────┘
pid ┴
st └─────────────────────────────┘
27 λ ⟨h₁, h₂⟩, by congr; assumption⟩
id ┴
src └───┘ └────────┘
typ ┴ └───┘ └────────┘
doc └────────┘
txt └───┘ └────────┘
par └───┘ └────────┘
st └────────────────┘
28
29 /-- Convert an integer to a `ℤ√d` -/
30 def of_int (n : ℤ) : ℤ√d := ⟨n, 0⟩
id ┴ └┘┴ ┴
src ┴ └┘
typ ┴ └┘┴ ┴
doc └┘
31 @[simp] theorem of_int_re (n : ℤ) : (of_int n).re = n := rfl
id ┴ └────┘ ┴ └┘ ┴ ┴ └─┘
src ┴ └────┘ └┘ ┴ └─┘
typ ┴ └────┘ ┴ └┘ ┴ ┴ └─┘
doc └──┘ └────┘
32 @[simp] theorem of_int_im (n : ℤ) : (of_int n).im = 0 := rfl
id ┴ └────┘ ┴ └┘ ┴ └─┘
src ┴ └────┘ └┘ ┴ └─┘
typ ┴ └────┘ ┴ └┘ ┴ └─┘
doc └──┘ └────┘
33
34 /-- The zero of the ring -/
35 def zero : ℤ√d := of_int 0
id └┘┴ └────┘
src └┘ └────┘
typ └┘┴ └────┘
doc └┘ └────┘
36 instance : has_zero ℤ√d := ⟨zsqrtd.zero⟩
id └──────┘ └┘┴ └─────────┘
src └──────┘ └┘ └─────────┘
typ └──────┘ └┘┴ └─────────┘
doc └┘ └─────────┘
37 @[simp] theorem zero_re : (0 : ℤ√d).re = 0 := rfl
id └┘┴ └┘ ┴ └─┘
src └┘ └┘ ┴ └─┘
typ └┘┴ └┘ ┴ └─┘
doc └──┘ └┘
38 @[simp] theorem zero_im : (0 : ℤ√d).im = 0 := rfl
id └┘┴ └┘ ┴ └─┘
src └┘ └┘ ┴ └─┘
typ └┘┴ └┘ ┴ └─┘
doc └──┘ └┘
39
40 instance : inhabited ℤ√d := ⟨0⟩
id └───────┘ └┘┴
src └───────┘ └┘
typ └───────┘ └┘┴
doc └┘
41
42 /-- The one of the ring -/
43 def one : ℤ√d := of_int 1
id └┘┴ └────┘
src └┘ └────┘
typ └┘┴ └────┘
doc └┘ └────┘
44 instance : has_one ℤ√d := ⟨zsqrtd.one⟩
id └─────┘ └┘┴ └────────┘
src └─────┘ └┘ └────────┘
typ └─────┘ └┘┴ └────────┘
doc └┘ └────────┘
45 @[simp] theorem one_re : (1 : ℤ√d).re = 1 := rfl
id └┘┴ └┘ ┴ └─┘
src └┘ └┘ ┴ └─┘
typ └┘┴ └┘ ┴ └─┘
doc └──┘ └┘
46 @[simp] theorem one_im : (1 : ℤ√d).im = 0 := rfl
id └┘┴ └┘ ┴ └─┘
src └┘ └┘ ┴ └─┘
typ └┘┴ └┘ ┴ └─┘
doc └──┘ └┘
47
48 /-- The representative of `√d` in the ring -/
49 def sqrtd : ℤ√d := ⟨0, 1⟩
id └┘┴
src └┘
typ └┘┴
doc └┘
50 @[simp] theorem sqrtd_re : (sqrtd : ℤ√d).re = 0 := rfl
id └───┘ └┘┴ └┘ ┴ └─┘
src └───┘ └┘ └┘ ┴ └─┘
typ └───┘ └┘┴ └┘ ┴ └─┘
doc └──┘ └───┘ └┘
51 @[simp] theorem sqrtd_im : (sqrtd : ℤ√d).im = 1 := rfl
id └───┘ └┘┴ └┘ ┴ └─┘
src └───┘ └┘ └┘ ┴ └─┘
typ └───┘ └┘┴ └┘ ┴ └─┘
doc └──┘ └───┘ └┘
52
53 /-- Addition of elements of `ℤ√d` -/
54 def add : ℤ√d → ℤ√d → ℤ√d
id └┘┴ ┴ └┘┴ └┘┴
src └┘ └┘ └┘
typ └┘┴ ┴ └┘┴ └┘┴
doc └┘ └┘ └┘
55 | ⟨x, y⟩ ⟨x', y'⟩ := ⟨x + x', y + y'⟩
id ┴ ┴ └┘ └┘ ┴ ┴
src ┴ ┴
typ ┴ ┴ └┘ └┘ ┴ ┴
56 instance : has_add ℤ√d := ⟨zsqrtd.add⟩
id └─────┘ └┘┴ └────────┘
src └─────┘ └┘ └────────┘
typ └─────┘ └┘┴ └────────┘
doc └┘ └────────┘
57 @[simp] theorem add_def (x y x' y' : ℤ) :
id ┴
src ┴
typ ┴
doc └──┘
58 (⟨x, y⟩ + ⟨x', y'⟩ : ℤ√d) = ⟨x + x', y + y'⟩ := rfl
id ┴ ┴ ┴ └┘ └┘ └┘┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └─┘
src ┴ └┘ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ └┘ └┘ └┘┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └─┘
doc └┘
59 @[simp] theorem add_re : ∀ z w : ℤ√d, (z + w).re = z.re + w.re
id ┴ └┘┴ ┴ ┴ ┴ └┘ ┴ ┴└─┘ ┴ ┴└─┘
src └┘ ┴ └┘ ┴ └─┘ ┴ └─┘
typ ┴ └┘┴ ┴ ┴ ┴ └┘ ┴ ┴└─┘ ┴ ┴└─┘
doc └──┘ └┘
60 | ⟨x, y⟩ ⟨x', y'⟩ := rfl
id └─┘
src └─┘
typ └─┘
61 @[simp] theorem add_im : ∀ z w : ℤ√d, (z + w).im = z.im + w.im
id ┴ └┘┴ ┴ ┴ ┴ └┘ ┴ ┴└─┘ ┴ ┴└─┘
src └┘ ┴ └┘ ┴ └─┘ ┴ └─┘
typ ┴ └┘┴ ┴ ┴ ┴ └┘ ┴ ┴└─┘ ┴ ┴└─┘
doc └──┘ └┘
62 | ⟨x, y⟩ ⟨x', y'⟩ := rfl
id └─┘
src └─┘
typ └─┘
63
64 @[simp] theorem bit0_re (z) : (bit0 z : ℤ√d).re = bit0 z.re := add_re _ _
id └──┘ ┴ └┘┴ └┘ ┴ └──┘ ┴└─┘ └────┘
src └──┘ └┘ └┘ ┴ └──┘ └─┘ └────┘
typ └──┘ ┴ └┘┴ └┘ ┴ └──┘ ┴└─┘ └────┘
doc └──┘ └┘
65 @[simp] theorem bit0_im (z) : (bit0 z : ℤ√d).im = bit0 z.im := add_im _ _
id └──┘ ┴ └┘┴ └┘ ┴ └──┘ ┴└─┘ └────┘
src └──┘ └┘ └┘ ┴ └──┘ └─┘ └────┘
typ └──┘ ┴ └┘┴ └┘ ┴ └──┘ ┴└─┘ └────┘
doc └──┘ └┘
66
67 @[simp] theorem bit1_re (z) : (bit1 z : ℤ√d).re = bit1 z.re := by simp [bit1]
id └──┘ ┴ └┘┴ └┘ ┴ └──┘ ┴└─┘ └──┘
src └──┘ └┘ └┘ ┴ └──┘ └─┘ └────┘└──┘└─
typ └──┘ ┴ └┘┴ └┘ ┴ └──┘ ┴└─┘ └────┘└──┘└─
doc └──┘ └┘ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────
68 @[simp] theorem bit1_im (z) : (bit1 z : ℤ√d).im = bit0 z.im := by simp [bit1]
id └──┘ ┴ └┘┴ └┘ ┴ └──┘ ┴└─┘ └──┘
src ─┘ └──┘ └┘ └┘ ┴ └──┘ └─┘ └────┘└──┘└─
typ ─┘ └──┘ ┴ └┘┴ └┘ ┴ └──┘ ┴└─┘ └────┘└──┘└─
doc ─┘ └──┘ └┘ └────┘ └─
txt ─┘ └────┘ └─
par ─┘ └────┘ └─
pid ─┘ ┴┴ ┴└
st ─┘ └────────────
69
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
70 /-- Negation in `ℤ√d` -/
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
71 def neg : ℤ√d → ℤ√d
id └┘┴ ┴ └┘┴
src └┘ └┘
typ └┘┴ ┴ └┘┴
doc └┘ └┘
72 | ⟨x, y⟩ := ⟨-x, -y⟩
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
73 instance : has_neg ℤ√d := ⟨zsqrtd.neg⟩
id └─────┘ └┘┴ └────────┘
src └─────┘ └┘ └────────┘
typ └─────┘ └┘┴ └────────┘
doc └┘ └────────┘
74 @[simp] theorem neg_re : ∀ z : ℤ√d, (-z).re = -z.re
id ┴ └┘┴ ┴┴ └┘ ┴ ┴┴└─┘
src └┘ ┴ └┘ ┴ ┴ └─┘
typ ┴ └┘┴ ┴┴ └┘ ┴ ┴┴└─┘
doc └──┘ └┘
75 | ⟨x, y⟩ := rfl
id └─┘
src └─┘
typ └─┘
76 @[simp] theorem neg_im : ∀ z : ℤ√d, (-z).im = -z.im
id ┴ └┘┴ ┴┴ └┘ ┴ ┴┴└─┘
src └┘ ┴ └┘ ┴ ┴ └─┘
typ ┴ └┘┴ ┴┴ └┘ ┴ ┴┴└─┘
doc └──┘ └┘
77 | ⟨x, y⟩ := rfl
id └─┘
src └─┘
typ └─┘
78
79 /-- Conjugation in `ℤ√d`. The conjugate of `a + b √d` is `a - b √d`. -/
80 def conj : ℤ√d → ℤ√d
id └┘┴ ┴ └┘┴
src └┘ └┘
typ └┘┴ ┴ └┘┴
doc └┘ └┘
81 | ⟨x, y⟩ := ⟨x, -y⟩
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
82 @[simp] theorem conj_re : ∀ z : ℤ√d, (conj z).re = z.re
id ┴ └┘┴ └──┘ ┴ └┘ ┴ ┴└─┘
src └┘ └──┘ └┘ ┴ └─┘
typ ┴ └┘┴ └──┘ ┴ └┘ ┴ ┴└─┘
doc └──┘ └┘ └──┘
83 | ⟨x, y⟩ := rfl
id └─┘
src └─┘
typ └─┘
84 @[simp] theorem conj_im : ∀ z : ℤ√d, (conj z).im = -z.im
id ┴ └┘┴ └──┘ ┴ └┘ ┴ ┴┴└─┘
src └┘ └──┘ └┘ ┴ ┴ └─┘
typ ┴ └┘┴ └──┘ ┴ └┘ ┴ ┴┴└─┘
doc └──┘ └┘ └──┘
85 | ⟨x, y⟩ := rfl
id └─┘
src └─┘
typ └─┘
86
87 /-- Multiplication in `ℤ√d` -/
88 def mul : ℤ√d → ℤ√d → ℤ√d
id └┘┴ ┴ └┘┴ └┘┴
src └┘ └┘ └┘
typ └┘┴ ┴ └┘┴ └┘┴
doc └┘ └┘ └┘
89 | ⟨x, y⟩ ⟨x', y'⟩ := ⟨x * x' + d * y * y', x * y' + y * x'⟩
id ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
90 instance : has_mul ℤ√d := ⟨zsqrtd.mul⟩
id └─────┘ └┘┴ └────────┘
src └─────┘ └┘ └────────┘
typ └─────┘ └┘┴ └────────┘
doc └┘ └────────┘
91 @[simp] theorem mul_re : ∀ z w : ℤ√d, (z * w).re = z.re * w.re + d * z.im * w.im
id ┴ └┘┴ ┴ ┴ ┴ └┘ ┴ ┴└─┘ ┴ ┴└─┘ ┴ ┴ ┴ ┴└─┘ ┴ ┴└─┘
src └┘ ┴ └┘ ┴ └─┘ ┴ └─┘ ┴ ┴ └─┘ ┴ └─┘
typ ┴ └┘┴ ┴ ┴ ┴ └┘ ┴ ┴└─┘ ┴ ┴└─┘ ┴ ┴ ┴ ┴└─┘ ┴ ┴└─┘
doc └──┘ └┘
92 | ⟨x, y⟩ ⟨x', y'⟩ := rfl
id └─┘
src └─┘
typ └─┘
93 @[simp] theorem mul_im : ∀ z w : ℤ√d, (z * w).im = z.re * w.im + z.im * w.re
id ┴ └┘┴ ┴ ┴ ┴ └┘ ┴ ┴└─┘ ┴ ┴└─┘ ┴ ┴└─┘ ┴ ┴└─┘
src └┘ ┴ └┘ ┴ └─┘ ┴ └─┘ ┴ └─┘ ┴ └─┘
typ ┴ └┘┴ ┴ ┴ ┴ └┘ ┴ ┴└─┘ ┴ ┴└─┘ ┴ ┴└─┘ ┴ ┴└─┘
doc └──┘ └┘
94 | ⟨x, y⟩ ⟨x', y'⟩ := rfl
id └─┘
src └─┘
typ └─┘
95
96 instance : comm_ring ℤ√d := by refine
id └───────┘ └┘┴
src └───────┘ └┘ └──────
typ └───────┘ └┘┴ └──────
doc └┘ └──────
txt └──────
par └──────
pid └
st └───────
97 { add := (+),
id ┴
src ─┘ └─────────────────┘┴└───
typ ─┘ └─────────────────┘┴└───
doc ─┘ └─────────────────┘ └───
txt ─┘ └─────────────────┘ └───
par ─┘ └─────────────────┘ └───
pid ─┘ └─────────────────┘ └───
st ───────────────────────────
98 zero := 0,
src ─────────────────────────
typ ─────────────────────────
doc ─────────────────────────
txt ─────────────────────────
par ─────────────────────────
pid ─────────────────────────
st ─────────────────────────
99 neg := has_neg.neg,
id └─────────┘
src ─────────────────────┘└─────────┘└─
typ ─────────────────────┘└─────────┘└─
doc ─────────────────────┘ └─
txt ─────────────────────┘ └─
par ─────────────────────┘ └─
pid ─────────────────────┘ └─
st ───────────────────────────────────
100 mul := (*),
id ┴
src ─────────────────────┘┴└───
typ ─────────────────────┘┴└───
doc ─────────────────────┘ └───
txt ─────────────────────┘ └───
par ─────────────────────┘ └───
pid ─────────────────────┘ └───
st ───────────────────────────
101 one := 1, ..};
src ───────────────────────────┘
typ ───────────────────────────┘
doc ───────────────────────────┘
txt ───────────────────────────┘
par ───────────────────────────┘
pid ───────────────────────────┘
st ──────────────────────────────
102 { intros, simp [ext, add_mul, mul_add, mul_comm, mul_left_comm] }
id └─┘ └─────┘ └─────┘ └──────┘ └───────────┘
src └────┘ └────┘└─┘└┘└─────┘└┘└─────┘└┘└──────┘└┘└───────────┘└┘
typ └────┘ └────┘└─┘└┘└─────┘└┘└─────┘└┘└──────┘└┘└───────────┘└┘
doc └────┘ └────┘ └┘ └┘ └┘ └┘ └┘
txt └────┘ └────┘ └┘ └┘ └┘ └┘ └┘
par └────┘ └────┘ └┘ └┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ └┘ └┘ ┴┴
st ─┘└──────┘└──────────────────────────────────────────────────────┘└┘
103
104 instance : add_comm_monoid ℤ√d := by apply_instance
id └─────────────┘ └┘┴
src └─────────────┘ └┘ └──────────────
typ └─────────────┘ └┘┴ └──────────────
doc └┘ └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
105 instance : add_monoid ℤ√d := by apply_instance
id └────────┘ └┘┴
src ─┘ └────────┘ └┘ └──────────────
typ ─┘ └────────┘ └┘┴ └──────────────
doc ─┘ └┘ └──────────────
txt ─┘ └──────────────
par ─┘ └──────────────
pid ─┘ └
st ─┘ └───────────────
106 instance : monoid ℤ√d := by apply_instance
id └────┘ └┘┴
src ─┘ └────┘ └┘ └──────────────
typ ─┘ └────┘ └┘┴ └──────────────
doc ─┘ └┘ └──────────────
txt ─┘ └──────────────
par ─┘ └──────────────
pid ─┘ └
st ─┘ └───────────────
107 instance : comm_monoid ℤ√d := by apply_instance
id └─────────┘ └┘┴
src ─┘ └─────────┘ └┘ └──────────────
typ ─┘ └─────────┘ └┘┴ └──────────────
doc ─┘ └┘ └──────────────
txt ─┘ └──────────────
par ─┘ └──────────────
pid ─┘ └
st ─┘ └───────────────
108 instance : comm_semigroup ℤ√d := by apply_instance
id └────────────┘ └┘┴
src ─┘ └────────────┘ └┘ └──────────────
typ ─┘ └────────────┘ └┘┴ └──────────────
doc ─┘ └┘ └──────────────
txt ─┘ └──────────────
par ─┘ └──────────────
pid ─┘ └
st ─┘ └───────────────
109 instance : semigroup ℤ√d := by apply_instance
id └───────┘ └┘┴
src ─┘ └───────┘ └┘ └──────────────
typ ─┘ └───────┘ └┘┴ └──────────────
doc ─┘ └┘ └──────────────
txt ─┘ └──────────────
par ─┘ └──────────────
pid ─┘ └
st ─┘ └───────────────
110 instance : add_comm_semigroup ℤ√d := by apply_instance
id └────────────────┘ └┘┴
src ─┘ └────────────────┘ └┘ └──────────────
typ ─┘ └────────────────┘ └┘┴ └──────────────
doc ─┘ └┘ └──────────────
txt ─┘ └──────────────
par ─┘ └──────────────
pid ─┘ └
st ─┘ └───────────────
111 instance : add_semigroup ℤ√d := by apply_instance
id └───────────┘ └┘┴
src ─┘ └───────────┘ └┘ └──────────────
typ ─┘ └───────────┘ └┘┴ └──────────────
doc ─┘ └┘ └──────────────
txt ─┘ └──────────────
par ─┘ └──────────────
pid ─┘ └
st ─┘ └───────────────
112 instance : comm_semiring ℤ√d := by apply_instance
id └───────────┘ └┘┴
src ─┘ └───────────┘ └┘ └──────────────
typ ─┘ └───────────┘ └┘┴ └──────────────
doc ─┘ └┘ └──────────────
txt ─┘ └──────────────
par ─┘ └──────────────
pid ─┘ └
st ─┘ └───────────────
113 instance : semiring ℤ√d := by apply_instance
id └──────┘ └┘┴
src ─┘ └──────┘ └┘ └──────────────
typ ─┘ └──────┘ └┘┴ └──────────────
doc ─┘ └┘ └──────────────
txt ─┘ └──────────────
par ─┘ └──────────────
pid ─┘ └
st ─┘ └───────────────
114 instance : ring ℤ√d := by apply_instance
id └──┘ └┘┴
src ─┘ └──┘ └┘ └──────────────
typ ─┘ └──┘ └┘┴ └──────────────
doc ─┘ └┘ └──────────────
txt ─┘ └──────────────
par ─┘ └──────────────
pid ─┘ └
st ─┘ └───────────────
115 instance : distrib ℤ√d := by apply_instance
id └─────┘ └┘┴
src ─┘ └─────┘ └┘ └──────────────
typ ─┘ └─────┘ └┘┴ └──────────────
doc ─┘ └┘ └──────────────
txt ─┘ └──────────────
par ─┘ └──────────────
pid ─┘ └
st ─┘ └───────────────
116
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
117 instance : zero_ne_one_class ℤ√d :=
id └───────────────┘ └┘┴
src ─┘ └───────────────┘ └┘
typ ─┘ └───────────────┘ └┘┴
doc ─┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
118 { zero := 0, one := 1, zero_ne_one := dec_trivial }
id └─────────┘
src └─────────┘
typ └─────────┘
doc └─────────┘
119
120 instance : nonzero_comm_ring ℤ√d :=
id └───────────────┘ └┘┴
src └───────────────┘ └┘
typ └───────────────┘ └┘┴
doc └───────────────┘ └┘
121 { ..zsqrtd.comm_ring, ..zsqrtd.zero_ne_one_class }
id └──────────────┘ └──────────────────────┘
src └──────────────┘ └──────────────────────┘
typ └──────────────┘ └──────────────────────┘
122
123 @[simp] theorem coe_nat_re (n : ℕ) : (n : ℤ√d).re = n :=
id ┴ ┴ └┘┴ └┘ ┴ ┴
src ┴ └┘ └┘ ┴
typ ┴ ┴ └┘┴ └┘ ┴ ┴
doc └──┘ └┘
124 by induction n; simp *
id ┴
src └────────┘ └──────
typ └────────┘┴ └──────
doc └────────┘ └──────
txt └────────┘ └──────
par └────────┘ └──────
pid ┴ ┴┴└
st └────────────────────
125 @[simp] theorem coe_nat_im (n : ℕ) : (n : ℤ√d).im = 0 :=
id ┴ ┴ └┘┴ └┘ ┴
src ─┘ ┴ └┘ └┘ ┴
typ ─┘ ┴ ┴ └┘┴ └┘ ┴
doc ─┘ └──┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
126 by induction n; simp *
id ┴
src └────────┘ └──────
typ └────────┘┴ └──────
doc └────────┘ └──────
txt └────────┘ └──────
par └────────┘ └──────
pid ┴ ┴┴└
st └────────────────────
127 theorem coe_nat_val (n : ℕ) : (n : ℤ√d) = ⟨n, 0⟩ :=
id ┴ ┴ └┘┴ ┴ ┴
src ─┘ ┴ └┘ ┴
typ ─┘ ┴ ┴ └┘┴ ┴ ┴
doc ─┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
128 by simp [ext]
id └─┘
src └────┘└─┘└─
typ └────┘└─┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
129
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
130 @[simp] theorem coe_int_re (n : ℤ) : (n : ℤ√d).re = n :=
id ┴ ┴ └┘┴ └┘ ┴ ┴
src ─┘ ┴ └┘ └┘ ┴
typ ─┘ ┴ ┴ └┘┴ └┘ ┴ ┴
doc ─┘ └──┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
131 by cases n; simp [*, int.of_nat_eq_coe, int.neg_succ_of_nat_eq]
id ┴ └───────────────┘ └────────────────────┘
src └────┘ └───────┘└───────────────┘└┘└────────────────────┘└─
typ └────┘┴ └───────┘└───────────────┘└┘└────────────────────┘└─
doc └────┘ └───────┘ └┘ └─
txt └────┘ └───────┘ └┘ └─
par └────┘ └───────┘ └┘ └─
pid ┴ ┴└──┘ └┘ ┴└
st └─────────────────────────────────────────────────────────────
132 @[simp] theorem coe_int_im (n : ℤ) : (n : ℤ√d).im = 0 :=
id ┴ ┴ └┘┴ └┘ ┴
src ─┘ ┴ └┘ └┘ ┴
typ ─┘ ┴ ┴ └┘┴ └┘ ┴
doc ─┘ └──┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
133 by cases n; simp *
id ┴
src └────┘ └──────
typ └────┘┴ └──────
doc └────┘ └──────
txt └────┘ └──────
par └────┘ └──────
pid ┴ ┴┴└
st └────────────────
134 theorem coe_int_val (n : ℤ) : (n : ℤ√d) = ⟨n, 0⟩ :=
id ┴ ┴ └┘┴ ┴ ┴
src ─┘ ┴ └┘ ┴
typ ─┘ ┴ ┴ └┘┴ ┴ ┴
doc ─┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
135 by simp [ext]
id └─┘
src └────┘└─┘└─
typ └────┘└─┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
136
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
137 instance : char_zero ℤ√d :=
id └───────┘ └┘┴
src ─┘ └───────┘ └┘
typ ─┘ └───────┘ └┘┴
doc ─┘ └───────┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
138 { cast_injective := λ m n, by simp [ext] }
id ┴ ┴ └─┘
src └────┘└─┘└┘
typ ┴ ┴ └────┘└─┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └──────────┘
139
140 @[simp] theorem of_int_eq_coe (n : ℤ) : (of_int n : ℤ√d) = n :=
id ┴ └────┘ ┴ └┘┴ ┴ ┴
src ┴ └────┘ └┘ ┴
typ ┴ └────┘ ┴ └┘┴ ┴ ┴
doc └──┘ └────┘ └┘
141 by simp [ext]
id └─┘
src └────┘└─┘└─
typ └────┘└─┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
142
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
143 @[simp] theorem smul_val (n x y : ℤ) : (n : ℤ√d) * ⟨x, y⟩ = ⟨n * x, n * y⟩ :=
id ┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ─┘ ┴ └┘ ┴ ┴ ┴ ┴
typ ─┘ ┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ─┘ └──┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
144 by simp [ext]
id └─┘
src └────┘└─┘└─
typ └────┘└─┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
145
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
146 @[simp] theorem muld_val (x y : ℤ) : sqrtd * ⟨x, y⟩ = ⟨d * y, x⟩ :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ─┘ ┴ └───┘ ┴ ┴ ┴
typ ─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ─┘ └──┘ └───┘
txt ─┘
par ─┘
pid ─┘
st ─┘
147 by simp [ext]
id └─┘
src └────┘└─┘└─
typ └────┘└─┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
148
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
149 @[simp] theorem smuld_val (n x y : ℤ) : sqrtd * (n : ℤ√d) * ⟨x, y⟩ = ⟨d * n * y, n * x⟩ :=
id ┴ └───┘ ┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ─┘ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴
typ ─┘ ┴ └───┘ ┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ─┘ └──┘ └───┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
150 by simp [ext]
id └─┘
src └────┘└─┘└─
typ └────┘└─┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
151
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
152 theorem decompose {x y : ℤ} : (⟨x, y⟩ : ℤ√d) = x + sqrtd * y :=
id ┴ ┴ ┴ └┘┴ ┴ ┴ ┴ └───┘ ┴ ┴
src ─┘ ┴ └┘ ┴ ┴ └───┘ ┴
typ ─┘ ┴ ┴ ┴ └┘┴ ┴ ┴ ┴ └───┘ ┴ ┴
doc ─┘ └┘ └───┘
txt ─┘
par ─┘
pid ─┘
st ─┘
153 by simp [ext]
id └─┘
src └────┘└─┘└─
typ └────┘└─┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
154
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
155 theorem mul_conj {x y : ℤ} : (⟨x, y⟩ * conj ⟨x, y⟩ : ℤ√d) = x * x - d * y * y :=
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ─┘ ┴ ┴ └──┘ └┘ ┴ ┴ ┴ ┴ ┴
typ ─┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ─┘ └──┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
156 by simp [ext, mul_comm]
id └─┘ └──────┘
src └────┘└─┘└┘└──────┘└─
typ └────┘└─┘└┘└──────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └─────────────────────
157
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
158 theorem conj_mul : Π {a b : ℤ√d}, conj (a * b) = conj a * conj b :=
id └┘┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src ─┘ └┘ └──┘ ┴ ┴ └──┘ ┴ └──┘
typ ─┘ └┘┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc ─┘ └┘ └──┘ └──┘ └──┘
txt ─┘
par ─┘
pid ─┘
st ─┘
159 by simp [ext]
id └─┘
src └────┘└─┘└─
typ └────┘└─┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
160
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
161 protected lemma coe_int_add (m n : ℤ) : (↑(m + n) : ℤ√d) = ↑m + ↑n := by simp [ext]
id ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴┴ ┴ ┴┴ └─┘
src ─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────┘└─┘└─
typ ─┘ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴┴ ┴ ┴┴ └────┘└─┘└─
doc ─┘ └┘ └────┘ └─
txt ─┘ └────┘ └─
par ─┘ └────┘ └─
pid ─┘ ┴┴ ┴└
st ─┘ └───────────
162 protected lemma coe_int_sub (m n : ℤ) : (↑(m - n) : ℤ√d) = ↑m - ↑n := by simp [ext]
id ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴┴ ┴ ┴┴ └─┘
src ─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────┘└─┘└─
typ ─┘ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴┴ ┴ ┴┴ └────┘└─┘└─
doc ─┘ └┘ └────┘ └─
txt ─┘ └────┘ └─
par ─┘ └────┘ └─
pid ─┘ ┴┴ ┴└
st ─┘ └───────────
163 protected lemma coe_int_mul (m n : ℤ) : (↑(m * n) : ℤ√d) = ↑m * ↑n := by simp [ext]
id ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴┴ ┴ ┴┴ └─┘
src ─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────┘└─┘└─
typ ─┘ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴┴ ┴ ┴┴ └────┘└─┘└─
doc ─┘ └┘ └────┘ └─
txt ─┘ └────┘ └─
par ─┘ └────┘ └─
pid ─┘ ┴┴ ┴└
st ─┘ └───────────
164 protected lemma coe_int_inj {m n : ℤ} (h : (↑m : ℤ√d) = ↑n) : m = n :=
id ┴ ┴┴ └┘┴ ┴ ┴┴ ┴ ┴ ┴
src ─┘ ┴ ┴ └┘ ┴ ┴ ┴
typ ─┘ ┴ ┴┴ └┘┴ ┴ ┴┴ ┴ ┴ ┴
doc ─┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
165 by simpa using congr_arg re h
id └───────┘ └┘ ┴
src └──────────┘└───────┘┴└┘┴ └
typ └──────────┘└───────┘┴└┘┴┴└
doc └──────────┘ ┴ ┴ └
txt └──────────┘ ┴ ┴ └
par └──────────┘ ┴ ┴ └
pid ┴└────┘ ┴ ┴ └
st └───────────────────────────
166
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
167 /-- Read `sq_le a c b d` as `a √c ≤ b √d` -/
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
168 def sq_le (a c b d : ℕ) : Prop := c*a*a ≤ d*b*b
id ┴ ┴┴┴┴┴ ┴ ┴┴┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴┴┴┴ ┴ ┴┴┴┴┴
169
170 theorem sq_le_of_le {c d x y z w : ℕ} (xz : z ≤ x) (yw : y ≤ w) (xy : sq_le x c y d) : sq_le z c w d :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └───┘ └───┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
doc └───┘ └───┘
171 le_trans (mul_le_mul (nat.mul_le_mul_left _ xz) xz (nat.zero_le _) (nat.zero_le _)) $
id └──────┘ └────────┘ └─────────────────┘ └┘ └┘ └─────────┘ └─────────┘
src └──────┘ └────────┘ └─────────────────┘ └─────────┘ └─────────┘
typ └──────┘ └────────┘ └─────────────────┘ └┘ └┘ └─────────┘ └─────────┘
172 le_trans xy (mul_le_mul (nat.mul_le_mul_left _ yw) yw (nat.zero_le _) (nat.zero_le _))
id └──────┘ └┘ └────────┘ └─────────────────┘ └┘ └┘ └─────────┘ └─────────┘
src └──────┘ └────────┘ └─────────────────┘ └─────────┘ └─────────┘
typ └──────┘ └┘ └────────┘ └─────────────────┘ └┘ └┘ └─────────┘ └─────────┘
173
174 theorem sq_le_add_mixed {c d x y z w : ℕ} (xy : sq_le x c y d) (zw : sq_le z c w d) :
id ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src ┴ └───┘ └───┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
doc └───┘ └───┘
175 c * (x * z) ≤ d * (y * w) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
176 nat.mul_self_le_mul_self_iff.2 $
id └──────────────────────────┘┴
src └──────────────────────────┘┴
typ └──────────────────────────┘┴
177 by simpa [mul_comm, mul_left_comm] using
id └──────┘ └───────────┘
src └─────┘└──────┘└┘└───────────┘└───────
typ └─────┘└──────┘└┘└───────────┘└───────
doc └─────┘ └┘ └───────
txt └─────┘ └┘ └───────
par └─────┘ └┘ └───────
pid ┴┴ └┘ ┴┴└─────
st └──────────────────────────────────────
178 mul_le_mul xy zw (nat.zero_le _) (nat.zero_le _)
id └────────┘ └┘ └┘ └─────────┘
src ────┘└────────┘┴ ┴ ┴ └──┘ └─────────┘└───
typ ────┘└────────┘┴└┘┴└┘┴ └──┘ └─────────┘└───
doc ────┘ ┴ ┴ ┴ └──┘ └───
txt ────┘ ┴ ┴ ┴ └──┘ └───
par ────┘ ┴ ┴ ┴ └──┘ └───
pid ────┘ ┴ ┴ ┴ └──┘ └─┘└
st ──────────────────────────────────────────────────────
179
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
180 theorem sq_le_add {c d x y z w : ℕ} (xy : sq_le x c y d) (zw : sq_le z c w d) :
id ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src ─┘ ┴ └───┘ └───┘
typ ─┘ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
doc ─┘ └───┘ └───┘
txt ─┘
par ─┘
pid ─┘
st ─┘
181 sq_le (x + z) c (y + w) d :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
182 begin
st └─────
183 have xz := sq_le_add_mixed xy zw,
id └─────────────┘ └┘ └┘
src └─────────┘└─────────────┘┴ ┴
typ └─────────┘└─────────────┘┴└┘┴└┘
doc └─────────┘ ┴ ┴
txt └─────────┘ ┴ ┴
par └─────────┘ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴
st ───────────────────────────────────┘└─
184 simp [sq_le, mul_assoc] at xy zw,
id └───┘ └───────┘
src └────┘└───┘└┘└───────┘└────────┘
typ └────┘└───┘└┘└───────┘└────────┘
doc └────┘└───┘└┘ └────────┘
txt └────┘ └┘ └────────┘
par └────┘ └┘ └────────┘
pid ┴┴ └┘ ┴┴└──────┘
st ───────────────────────────────────┘└─
185 simp [sq_le, mul_add, mul_comm, mul_left_comm, add_le_add, *]
id └───┘ └─────┘ └──────┘ └───────────┘ └────────┘
src └────┘└───┘└┘└─────┘└┘└──────┘└┘└───────────┘└┘└────────┘└────
typ └────┘└───┘└┘└─────┘└┘└──────┘└┘└───────────┘└┘└────────┘└────
doc └────┘└───┘└┘ └┘ └┘ └┘ └────
txt └────┘ └┘ └┘ └┘ └┘ └────
par └────┘ └┘ └┘ └┘ └┘ └────
pid ┴┴ └┘ └┘ └┘ └┘ └──┘└
st ──────────────────────────────────────────────────────────────────
186 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
187
188 theorem sq_le_cancel {c d x y z w : ℕ} (zw : sq_le y d x c) (h : sq_le (x + z) c (y + w) d) : sq_le z c w d :=
id ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src ┴ └───┘ └───┘ ┴ ┴ └───┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
doc └───┘ └───┘ └───┘
189 begin
st └─────
190 apply le_of_not_gt,
id └──────────┘
src └────┘└──────────┘
typ └────┘└──────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
191 intro l,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ──────────┘└─
192 refine not_le_of_gt _ h,
id └──────────┘ ┴
src └─────┘└──────────┘└─┘
typ └─────┘└──────────┘└─┘┴
doc └─────┘ └─┘
txt └─────┘ └─┘
par └─────┘ └─┘
pid ┴ └─┘
st ──────────────────────────┘└─
193 simp [sq_le, mul_add, mul_comm, mul_left_comm],
id └───┘ └─────┘ └──────┘ └───────────┘
src └────┘└───┘└┘└─────┘└┘└──────┘└┘└───────────┘┴
typ └────┘└───┘└┘└─────┘└┘└──────┘└┘└───────────┘┴
doc └────┘└───┘└┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ └┘ ┴
par └────┘ └┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ └┘ ┴
st ─────────────────────────────────────────────────┘└─
194 have hm := sq_le_add_mixed zw (le_of_lt l),
id └─────────────┘ └┘ └──────┘ ┴
src └─────────┘└─────────────┘┴ ┴ └──────┘┴ ┴
typ └─────────┘└─────────────┘┴└┘┴ └──────┘┴┴┴
doc └─────────┘ ┴ ┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────┘└─
195 simp [sq_le, mul_assoc] at l zw,
id └───┘ └───────┘
src └────┘└───┘└┘└───────┘└───────┘
typ └────┘└───┘└┘└───────┘└───────┘
doc └────┘└───┘└┘ └───────┘
txt └────┘ └┘ └───────┘
par └────┘ └┘ └───────┘
pid ┴┴ └┘ ┴┴└─────┘
st ──────────────────────────────────┘└─
196 exact lt_of_le_of_lt (add_le_add_right zw _)
id └────────────┘ └──────────────┘ └┘
src └────┘└────────────┘┴ └──────────────┘┴ └───
typ └────┘└────────────┘┴ └──────────────┘┴└┘└───
doc └────┘ ┴ ┴ └───
txt └────┘ ┴ ┴ └───
par └────┘ ┴ ┴ └───
pid ┴ ┴ ┴ └───
st ─────────────────────────────────────────────────
197 (add_lt_add_left (add_lt_add_of_le_of_lt hm (add_lt_add_of_le_of_lt hm l)) _)
id └─────────────┘ └────────────────────┘ └┘ ┴
src ─────┘ └─────────────┘┴ ┴ ┴ └────────────────────┘┴ ┴ └─────
typ ─────┘ └─────────────┘┴ ┴ ┴ └────────────────────┘┴└┘┴┴└─────
doc ─────┘ ┴ ┴ ┴ ┴ ┴ └─────
txt ─────┘ ┴ ┴ ┴ ┴ ┴ └─────
par ─────┘ ┴ ┴ ┴ ┴ ┴ └─────
pid ─────┘ ┴ ┴ ┴ ┴ ┴ └───┘└
st ────────────────────────────────────────────────────────────────────────────────────
198 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
199
200 theorem sq_le_smul {c d x y : ℕ} (n : ℕ) (xy : sq_le x c y d) : sq_le (n * x) c (n * y) d :=
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └───┘ └───┘ ┴ ┴
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘
201 by simpa [sq_le, mul_left_comm, mul_assoc] using
id └───┘ └───────────┘ └───────┘
src └─────┘└───┘└┘└───────────┘└┘└───────┘└───────
typ └─────┘└───┘└┘└───────────┘└┘└───────┘└───────
doc └─────┘└───┘└┘ └┘ └───────
txt └─────┘ └┘ └┘ └───────
par └─────┘ └┘ └┘ └───────
pid ┴┴ └┘ └┘ ┴┴└─────
st └──────────────────────────────────────────────
202 nat.mul_le_mul_left (n * n) xy
id └─────────────────┘ ┴ ┴ └┘
src ────┘└─────────────────┘┴ ┴┴┴ └┘ └
typ ────┘└─────────────────┘┴ ┴┴┴┴└┘└┘└
doc ────┘ ┴ ┴ ┴ └┘ └
txt ────┘ ┴ ┴ ┴ └┘ └
par ────┘ ┴ ┴ ┴ └┘ └
pid ────┘ ┴ ┴ ┴ └┘ └
st ────────────────────────────────────
203
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
204 theorem sq_le_mul {d x y z w : ℕ} :
id ┴
src ─┘ ┴
typ ─┘ ┴
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
205 (sq_le x 1 y d → sq_le z 1 w d → sq_le (x * w + y * z) d (x * z + d * y * w) 1) ∧
id └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └───┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘ └───┘
206 (sq_le x 1 y d → sq_le w d z 1 → sq_le (x * z + d * y * w) 1 (x * w + y * z) d) ∧
id └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └───┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘ └───┘
207 (sq_le y d x 1 → sq_le z 1 w d → sq_le (x * z + d * y * w) 1 (x * w + y * z) d) ∧
id └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └───┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘ └───┘
208 (sq_le y d x 1 → sq_le w d z 1 → sq_le (x * w + y * z) d (x * z + d * y * w) 1) :=
id └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └───┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘ └───┘
209 by refine ⟨_, _, _, _⟩; {
src └─────┘ └─────────┘
typ └─────┘ └─────────┘
doc └─────┘ └─────────┘
txt └─────┘ └─────────┘
par └─────┘ └─────────┘
pid ┴ └─────────┘
st └────────────────────┘└─
210 intros xy zw,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └────┘
st ───────────────┘└─
211 have := int.mul_nonneg (sub_nonneg_of_le (int.coe_nat_le_coe_nat_of_le xy))
id └────────────┘ └┘
src └──────┘└────────────┘┴ ┴ ┴ └──
typ └──────┘└────────────┘┴ ┴ ┴└┘└──
doc └──────┘ ┴ ┴ ┴ └──
txt └──────┘ ┴ ┴ ┴ └──
par └──────┘ ┴ ┴ ┴ └──
pid └───┘└─┘ ┴ ┴ ┴ └──
st ────────────────────────────────────────────────────────────────────────────────
212 (sub_nonneg_of_le (int.coe_nat_le_coe_nat_of_le zw)),
id └──────────────┘ └──────────────────────────┘ └┘
src ──────────────────────────┘ └──────────────┘┴ └──────────────────────────┘┴ └┘
typ ──────────────────────────┘ └──────────────┘┴ └──────────────────────────┘┴└┘└┘
doc ──────────────────────────┘ ┴ ┴ └┘
txt ──────────────────────────┘ ┴ ┴ └┘
par ──────────────────────────┘ ┴ ┴ └┘
pid ──────────────────────────┘ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────┘└─
213 refine int.le_of_coe_nat_le_coe_nat (le_of_sub_nonneg _),
id └──────────────────────────┘ └──────────────┘
src └─────┘└──────────────────────────┘┴ └──────────────┘└─┘
typ └─────┘└──────────────────────────┘┴ └──────────────┘└─┘
doc └─────┘ ┴ └─┘
txt └─────┘ ┴ └─┘
par └─────┘ ┴ └─┘
pid ┴ ┴ └─┘
st ───────────────────────────────────────────────────────────┘└─
214 simpa [mul_add, mul_left_comm, mul_comm] }
id └─────┘ └───────────┘ └──────┘
src └─────┘└─────┘└┘└───────────┘└┘└──────┘└┘
typ └─────┘└─────┘└┘└───────────┘└┘└──────┘└┘
doc └─────┘ └┘ └┘ └┘
txt └─────┘ └┘ └┘ └┘
par └─────┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ ┴┴
st ────────────────────────────────────────────┘└┘
215
216 /-- "Generalized" `nonneg`. `nonnegg c d x y` means `a √c + b √d ≥ 0`;
217 we are interested in the case `c = 1` but this is more symmetric -/
218 def nonnegg (c d : ℕ) : ℤ → ℤ → Prop
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
219 | (a : ℕ) (b : ℕ) := true
id ┴ ┴ └──┘
src ┴ ┴ └──┘
typ ┴ ┴ └──┘
220 | (a : ℕ) -[1+ b] := sq_le (b+1) c a d
id ┴ ┴ └──┘ ┴┴ └───┘ ┴ ┴ ┴
src ┴ └──┘ ┴ └───┘ ┴
typ ┴ ┴ └──┘ ┴┴ └───┘ ┴ ┴ ┴
doc └───┘
221 | -[1+ a] (b : ℕ) := sq_le (a+1) d b c
id └──┘ ┴┴ ┴ ┴ └───┘ ┴ ┴ ┴
src └──┘ ┴ ┴ └───┘ ┴
typ └──┘ ┴┴ ┴ ┴ └───┘ ┴ ┴ ┴
doc └───┘
222 | -[1+ a] -[1+ b] := false
id └──┘ ┴ └──┘ ┴ └───┘
src └──┘ ┴ └──┘ ┴ └───┘
typ └──┘ ┴ └──┘ ┴ └───┘
223
224 theorem nonnegg_comm {c d : ℕ} {x y : ℤ} : nonnegg c d x y = nonnegg d c y x :=
id ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src ┴ ┴ └─────┘ ┴ └─────┘
typ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘
225 by induction x; induction y; refl
id ┴ ┴
src └────────┘ └────────┘ └────
typ └────────┘┴ └────────┘┴ └────
doc └────────┘ └────────┘ └────
txt └────────┘ └────────┘ └────
par └────────┘ └────────┘ └────
pid ┴ ┴ └
st └───────────────────────────────
226
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
227 theorem nonnegg_neg_pos {c d} : Π {a b : ℕ}, nonnegg c d (-a) b ↔ sq_le a d b c
id ┴ ┴ └─────┘ ┴ ┴ ┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src ─┘ ┴ └─────┘ ┴ ┴ └───┘
typ ─┘ ┴ ┴ └─────┘ ┴ ┴ ┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
doc ─┘ └─────┘ └───┘
txt ─┘
par ─┘
pid ─┘
st ─┘
228 | 0 b := ⟨by simp [sq_le, nat.zero_le], λa, trivial⟩
id └───┘ └─────────┘ ┴ └─────┘
src └────┘└───┘└┘└─────────┘┴ └─────┘
typ └────┘└───┘└┘└─────────┘┴ ┴ └─────┘
doc └────┘└───┘└┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └────────────────────────┘
229 | (a+1) b := by rw ← int.neg_succ_of_nat_coe; refl
id ┴ └─────────────────────┘
src ┴ └───┘└─────────────────────┘ └────
typ ┴ └───┘└─────────────────────┘ └────
doc └───┘ └────
txt └───┘ └────
par └───┘ └────
pid └─┘ └
st └───────────────────────────────────
230
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
231 theorem nonnegg_pos_neg {c d} {a b : ℕ} : nonnegg c d a (-b) ↔ sq_le b c a d :=
id ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ └───┘ ┴ ┴ ┴ ┴
src ─┘ ┴ └─────┘ ┴ ┴ └───┘
typ ─┘ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ └───┘ ┴ ┴ ┴ ┴
doc ─┘ └─────┘ └───┘
txt ─┘
par ─┘
pid ─┘
st ─┘
232 by rw nonnegg_comm; exact nonnegg_neg_pos
id └──────────┘ └─────────────┘
src └─┘└──────────┘ └────┘└─────────────┘└
typ └─┘└──────────┘ └────┘└─────────────┘└
doc └─┘ └────┘ └
txt └─┘ └────┘ └
par └─┘ └────┘ └
pid ┴ ┴ └
st └───────────────────────────────────────
233
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
234 theorem nonnegg_cases_right {c d} {a : ℕ} : Π {b : ℤ}, (Π x : ℕ, b = -x → sq_le x c a d) → nonnegg c d a b
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src ─┘ ┴ ┴ ┴ ┴ ┴ └───┘ └─────┘
typ ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc ─┘ └───┘ └─────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
235 | (b:nat) h := trivial
id └─┘ └─────┘
src └─┘ └─────┘
typ └─┘ └─────┘
236 | -[1+ b] h := h (b+1) rfl
id └──┘ ┴┴ ┴ ┴ └─┘
src └──┘ ┴ ┴ └─┘
typ └──┘ ┴┴ ┴ ┴ └─┘
237
238 theorem nonnegg_cases_left {c d} {b : ℕ} {a : ℤ} (h : Π x : ℕ, a = -x → sq_le x d b c) : nonnegg c d a b :=
id ┴ ┴ ┴ ┴ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └───┘ └─────┘
typ ┴ ┴ ┴ ┴ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └───┘ └─────┘
239 cast nonnegg_comm (nonnegg_cases_right h)
id └──┘ └──────────┘ └─────────────────┘ ┴
src └──┘ └──────────┘ └─────────────────┘
typ └──┘ └──────────┘ └─────────────────┘ ┴
240
241 section norm
242
243 def norm (n : ℤ√d) : ℤ := n.re * n.re - d * n.im * n.im
id └┘┴ ┴ ┴└─┘ ┴ ┴└─┘ ┴ ┴ ┴ ┴└─┘ ┴ ┴└─┘
src └┘ ┴ └─┘ ┴ └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └┘┴ ┴ ┴└─┘ ┴ ┴└─┘ ┴ ┴ ┴ ┴└─┘ ┴ ┴└─┘
doc └┘
244
245 @[simp] lemma norm_zero : norm 0 = 0 := by simp [norm]
id └──┘ ┴ └──┘
src └──┘ ┴ └────┘└──┘└─
typ └──┘ ┴ └────┘└──┘└─
doc └──┘ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────
246
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
247 @[simp] lemma norm_one : norm 1 = 1 := by simp [norm]
id └──┘ ┴ └──┘
src └──┘ ┴ └────┘└──┘└─
typ └──┘ ┴ └────┘└──┘└─
doc └──┘ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────
248
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
249 @[simp] lemma norm_int_cast (n : ℤ) : norm n = n * n := by simp [norm]
id ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘
src ┴ └──┘ ┴ ┴ └────┘└──┘└─
typ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └────┘└──┘└─
doc └──┘ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────
250
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
251 @[simp] lemma norm_nat_cast (n : ℕ) : norm n = n * n := norm_int_cast n
id ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴
src ┴ └──┘ ┴ ┴ └───────────┘
typ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴
doc └──┘
252
253 @[simp] lemma norm_mul (n m : ℤ√d) : norm (n * m) = norm n * norm m :=
id └┘┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src └┘ └──┘ ┴ ┴ └──┘ ┴ └──┘
typ └┘┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └──┘ └┘
254 by simp [norm, mul_add, add_mul, mul_comm, mul_assoc, mul_left_comm]
id └──┘ └─────┘ └─────┘ └──────┘ └───────┘ └───────────┘
src └────┘└──┘└┘└─────┘└┘└─────┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
typ └────┘└──┘└┘└─────┘└┘└─────┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
doc └────┘ └┘ └┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ └┘ └┘ ┴└
st └──────────────────────────────────────────────────────────────────
255
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
256 lemma norm_eq_mul_conj (n : ℤ√d) : (norm n : ℤ√d) = n * n.conj :=
id └┘┴ └──┘ ┴ └┘┴ ┴ ┴ ┴ ┴└───┘
src └┘ └──┘ └┘ ┴ ┴ └───┘
typ └┘┴ └──┘ ┴ └┘┴ ┴ ┴ ┴ ┴└───┘
doc └┘ └┘ └───┘
257 by cases n; simp [norm, conj, zsqrtd.ext, mul_comm]
id ┴ └──┘ └──┘ └────────┘ └──────┘
src └────┘ └────┘└──┘└┘└──┘└┘└────────┘└┘└──────┘└─
typ └────┘┴ └────┘└──┘└┘└──┘└┘└────────┘└┘└──────┘└─
doc └────┘ └────┘ └┘└──┘└┘ └┘ └─
txt └────┘ └────┘ └┘ └┘ └┘ └─
par └────┘ └────┘ └┘ └┘ └┘ └─
pid ┴ ┴┴ └┘ └┘ └┘ ┴└
st └─────────────────────────────────────────────────
258
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
259 instance : is_monoid_hom norm :=
id └───────────┘ └──┘
src └───────────┘ └──┘
typ └───────────┘ └──┘
doc └───────────┘
260 { map_one := norm_one, map_mul := norm_mul }
id └──────┘ └──────┘
src └──────┘ └──────┘
typ └──────┘ └──────┘
261
262 lemma norm_nonneg (hd : d ≤ 0) (n : ℤ√d) : 0 ≤ n.norm :=
id ┴ ┴ └┘┴ ┴ ┴└───┘
src ┴ └┘ ┴ └───┘
typ ┴ ┴ └┘┴ ┴ ┴└───┘
doc └┘
263 add_nonneg (mul_self_nonneg _)
id └────────┘ └─────────────┘
src └────────┘ └─────────────┘
typ └────────┘ └─────────────┘
264 (by rw [mul_assoc, neg_mul_eq_neg_mul];
id └───────┘ └────────────────┘
src └──┘└───────┘└┘└────────────────┘┴
typ └──┘└───────┘└┘└────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └────────────┘└──────────────────┘┴└─
265 exact (mul_nonneg (neg_nonneg.2 hd) (mul_self_nonneg _)))
id └────────┘ └────────┘ └┘ └─────────────┘
src └────┘ └────────┘┴ └────────┘└─┘ └┘ └─────────────┘└──┘
typ └────┘ └────────┘┴ └────────┘└─┘└┘└┘ └─────────────┘└──┘
doc └────┘ ┴ └─┘ └┘ └──┘
txt └────┘ ┴ └─┘ └┘ └──┘
par └────┘ ┴ └─┘ └┘ └──┘
pid ┴ ┴ └─┘ └┘ └──┘
st ───────────────────────────────────────────────────────────┘
266
267 lemma norm_eq_one_iff {x : ℤ√d} : x.norm.nat_abs = 1 ↔ is_unit x :=
id └┘┴ ┴└───┘└──────┘ ┴ ┴ └─────┘ ┴
src └┘ └───┘└──────┘ ┴ ┴ └─────┘
typ └┘┴ ┴└───┘└──────┘ ┴ ┴ └─────┘ ┴
doc └┘ └─────┘
268 ⟨λ h, is_unit_iff_dvd_one.2 $
id ┴ └─────────────────┘┴
src └─────────────────┘┴
typ ┴ └─────────────────┘┴
269 (le_total 0 (norm x)).cases_on
id └──────┘ └──┘ ┴ └──────┘
src └──────┘ └──┘ └──────┘
typ └──────┘ └──┘ ┴ └──────┘
270 (λ hx, show x ∣ 1, from ⟨x.conj,
id └┘ ┴ ┴ ┴└───┘
src ┴ └───┘
typ └┘ ┴ ┴ ┴└───┘
doc └───┘
271 by rwa [← int.coe_nat_inj', int.nat_abs_of_nonneg hx,
id └──────────────┘ └───────────────────┘ └┘
src └─────┘└──────────────┘└┘└───────────────────┘┴ └─
typ └─────┘└──────────────┘└┘└───────────────────┘┴└┘└─
doc └─────┘ └┘ ┴ └─
txt └─────┘ └┘ ┴ └─
par └─────┘ └┘ ┴ └─
pid └──┘ └┘ ┴ └─
st └──────────────────────┘└────────────────────────┘└─
272 ← @int.cast_inj (ℤ√d) _ _, norm_eq_mul_conj, eq_comm] at h⟩)
id └──────────┘ ┴ └──────────────┘ └─────┘
src ─────────┘ └──────────┘┴ └─────┘└──────────────┘└┘└─────┘└────┘
typ ─────────┘ └──────────┘┴ ┴└─────┘└──────────────┘└┘└─────┘└────┘
doc ─────────┘ ┴ └─────┘ └┘ └────┘
txt ─────────┘ ┴ └─────┘ └┘ └────┘
par ─────────┘ ┴ └─────┘ └┘ └────┘
pid ─────────┘ ┴ └─────┘ └┘ ┴└───┘
st ────────────────────────────────┘└────────────────┘└───────┘┴└───┘
273 (λ hx, show x ∣ 1, from ⟨- x.conj,
id └┘ ┴ ┴ ┴ ┴└───┘
src ┴ ┴ └───┘
typ └┘ ┴ ┴ ┴ ┴└───┘
doc └───┘
274 by rwa [← int.coe_nat_inj', int.of_nat_nat_abs_of_nonpos hx,
id └──────────────┘ └──────────────────────────┘ └┘
src └─────┘└──────────────┘└┘└──────────────────────────┘┴ └─
typ └─────┘└──────────────┘└┘└──────────────────────────┘┴└┘└─
doc └─────┘ └┘ ┴ └─
txt └─────┘ └┘ ┴ └─
par └─────┘ └┘ ┴ └─
pid └──┘ └┘ ┴ └─
st └──────────────────────┘└───────────────────────────────┘└─
275 ← @int.cast_inj (ℤ√d) _ _, int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg,
id └──────────┘ ┴ └──────────┘ └──────────────┘ └────────────────┘
src ─────────┘ └──────────┘┴ └─────┘└──────────┘└┘└──────────────┘└┘└────────────────┘└─
typ ─────────┘ └──────────┘┴ ┴└─────┘└──────────┘└┘└──────────────┘└┘└────────────────┘└─
doc ─────────┘ ┴ └─────┘ └┘ └┘ └─
txt ─────────┘ ┴ └─────┘ └┘ └┘ └─
par ─────────┘ ┴ └─────┘ └┘ └┘ └─
pid ─────────┘ ┴ └─────┘ └┘ └┘ └─
st ────────────────────────────────┘└────────────┘└────────────────┘└──────────────────┘└─
276 eq_comm] at h⟩),
id └─────┘
src ───────┘└─────┘└────┘
typ ───────┘└─────┘└────┘
doc ───────┘ └────┘
txt ───────┘ └────┘
par ───────┘ └────┘
pid ───────┘ ┴└───┘
st ──────────────┘┴└───┘
277 λ h, let ⟨y, hy⟩ := is_unit_iff_dvd_one.1 h in begin
id ┴ └─┘ └─────────────────┘┴ ┴
src └─────────────────┘┴
typ ┴ └─┘ └─────────────────┘┴ ┴
st └─────
278 have := congr_arg (int.nat_abs ∘ norm) hy,
id └───────┘ └─────────┘ ┴ └──┘ └┘
src └──────┘└───────┘┴ └─────────┘┴┴┴└──┘└┘
typ └──────┘└───────┘┴ └─────────┘┴┴┴└──┘└┘└┘
doc └──────┘ ┴ ┴ ┴ └┘
txt └──────┘ ┴ ┴ ┴ └┘
par └──────┘ ┴ ┴ ┴ └┘
pid └───┘└─┘ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────┘└─
279 rw [function.comp_app, function.comp_app, norm_mul, int.nat_abs_mul,
id └───────────────┘ └───────────────┘ └──────┘ └─────────────┘
src └──┘└───────────────┘└┘└───────────────┘└┘└──────┘└┘└─────────────┘└─
typ └──┘└───────────────┘└┘└───────────────┘└┘└──────┘└┘└─────────────┘└─
doc └──┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └─
st ──────────────────────┘└─────────────────┘└────────┘└───────────────┘└─
280 norm_one, int.nat_abs_one, eq_comm, nat.mul_eq_one_iff] at this,
id └──────┘ └─────────────┘ └─────┘ └────────────────┘
src ───┘└──────┘└┘└─────────────┘└┘└─────┘└┘└────────────────┘└───────┘
typ ───┘└──────┘└┘└─────────────┘└┘└─────┘└┘└────────────────┘└───────┘
doc ───┘ └┘ └┘ └┘ └───────┘
txt ───┘ └┘ └┘ └┘ └───────┘
par ───┘ └┘ └┘ └┘ └───────┘
pid ───┘ └┘ └┘ └┘ ┴└──────┘
st ───────────┘└───────────────┘└───────┘└──────────────────┘┴└──────┘└─
281 exact this.1
id └──┘
src └────┘ └─┘
typ └────┘└──┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ──────────────┘
282 end⟩
st └─┘
283
284 end norm
285
286 end
287
288 section
289 parameter {d : ℕ}
id ┴
src ┴
typ ┴
290
291 /-- Nonnegativity of an element of `ℤ√d`. -/
292 def nonneg : ℤ√d → Prop | ⟨a, b⟩ := nonnegg d 1 a b
id └┘┴ ┴ ┴ ┴ └─────┘ ┴
src └┘ └─────┘
typ └┘┴ ┴ ┴ ┴ └─────┘ ┴
doc └┘ └─────┘
293
294 protected def le (a b : ℤ√d) : Prop := nonneg (b - a)
id └┘┴ └────┘ ┴ ┴ ┴
src └┘ └────┘ ┴
typ └┘┴ └────┘ ┴ ┴ ┴
doc └┘ └────┘
295
296 instance : has_le ℤ√d := ⟨zsqrtd.le⟩
id └────┘ └┘┴ └───────┘
src └────┘ └┘ └───────┘
typ └────┘ └┘┴ └───────┘
doc └┘
297
298 protected def lt (a b : ℤ√d) : Prop := ¬(b ≤ a)
id └┘┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴
typ └┘┴ ┴ ┴ ┴ ┴
doc └┘
299
300 instance : has_lt ℤ√d := ⟨zsqrtd.lt⟩
id └────┘ └┘┴ └───────┘
src └────┘ └┘ └───────┘
typ └────┘ └┘┴ └───────┘
doc └┘
301
302 instance decidable_nonnegg (c d a b) : decidable (nonnegg c d a b) :=
id └───────┘ └─────┘ ┴ ┴ ┴ ┴
src └───────┘ └─────┘
typ └───────┘ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘
303 by cases a; cases b; repeat {rw int.of_nat_eq_coe}; unfold nonnegg sq_le; apply_instance
id ┴ ┴ └───────────────┘
src └────┘ └────┘ └──────┘└─┘└───────────────┘┴ └──────────────────┘ └──────────────
typ └────┘┴ └────┘┴ └──────┘└─┘└───────────────┘┴ └──────────────────┘ └──────────────
doc └────┘ └────┘ └──────┘└─┘ ┴ └──────────────────┘ └──────────────
txt └────┘ └────┘ └──────┘└─┘ ┴ └──────────────────┘ └──────────────
par └────┘ └────┘ └──────┘└─┘ ┴ └──────────────────┘ └──────────────
pid ┴ ┴ └───┘ ┴ └────────────┘ └
st └─────────────────────────┘└──────────────────┘└┘└─────────────────────────────────────
304
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
305 instance decidable_nonneg : Π (a : ℤ√d), decidable (nonneg a)
id ┴ └┘┴ └───────┘ └────┘ ┴
src ─┘ └┘ └───────┘ └────┘
typ ─┘ ┴ └┘┴ └───────┘ └────┘ ┴
doc ─┘ └┘ └────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
306 | ⟨a, b⟩ := zsqrtd.decidable_nonnegg _ _ _ _
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
307
308 instance decidable_le (a b : ℤ√d) : decidable (a ≤ b) := decidable_nonneg _
id └┘┴ └───────┘ ┴ ┴ ┴ └──────────────┘
src └┘ └───────┘ ┴ └──────────────┘
typ └┘┴ └───────┘ ┴ ┴ ┴ └──────────────┘
doc └┘
309
310 theorem nonneg_cases : Π {a : ℤ√d}, nonneg a → ∃ x y : ℕ, a = ⟨x, y⟩ ∨ a = ⟨x, -y⟩ ∨ a = ⟨-x, y⟩
id ┴ └┘┴ └────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴
src └┘ └────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └┘┴ └────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴
doc └┘ └────┘
311 | ⟨(x : ℕ), (y : ℕ)⟩ h := ⟨x, y, or.inl rfl⟩
id ┴ ┴ ┴ ┴ └────┘ └─┘
src ┴ ┴ └────┘ └─┘
typ ┴ ┴ ┴ ┴ └────┘ └─┘
312 | ⟨(x : ℕ), -[1+ y]⟩ h := ⟨x, y+1, or.inr $ or.inl rfl⟩
id ┴ ┴ └──┘ ┴┴ ┴ └────┘ └────┘ └─┘
src ┴ └──┘ ┴ ┴ └────┘ └────┘ └─┘
typ ┴ ┴ └──┘ ┴┴ ┴ └────┘ └────┘ └─┘
313 | ⟨-[1+ x], (y : ℕ)⟩ h := ⟨x+1, y, or.inr $ or.inr rfl⟩
id └──┘ ┴┴ ┴ ┴ ┴ └────┘ └────┘ └─┘
src └──┘ ┴ ┴ ┴ └────┘ └────┘ └─┘
typ └──┘ ┴┴ ┴ ┴ ┴ └────┘ └────┘ └─┘
314 | ⟨-[1+ x], -[1+ y]⟩ h := false.elim h
id └──┘ ┴ └──┘ ┴ ┴ └────────┘
src └──┘ ┴ └──┘ ┴ └────────┘
typ └──┘ ┴ └──┘ ┴ ┴ └────────┘
315
316 lemma nonneg_add_lem {x y z w : ℕ} (xy : nonneg ⟨x, -y⟩) (zw : nonneg ⟨-z, w⟩) : nonneg (⟨x, -y⟩ + ⟨-z, w⟩) :=
id ┴ └────┘ ┴ ┴┴ └────┘ ┴┴ ┴ └────┘ ┴ ┴┴ ┴ ┴┴ ┴
src ┴ └────┘ ┴ └────┘ ┴ └────┘ ┴ ┴ ┴
typ ┴ └────┘ ┴ ┴┴ └────┘ ┴┴ ┴ └────┘ ┴ ┴┴ ┴ ┴┴ ┴
doc └────┘ └────┘ └────┘
317 have nonneg ⟨int.sub_nat_nat x z, int.sub_nat_nat w y⟩, from int.sub_nat_nat_elim x z
id └────┘ └─────────────┘ ┴ ┴ └─────────────┘ ┴ ┴ └──────────────────┘ ┴ ┴
src └────┘ └─────────────┘ └─────────────┘ └──────────────────┘
typ └────┘ └─────────────┘ ┴ ┴ └─────────────┘ ┴ ┴ └──────────────────┘ ┴ ┴
doc └────┘
318 (λm n i, sq_le y d m 1 → sq_le n 1 w d → nonneg ⟨i, int.sub_nat_nat w y⟩)
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └────┘ ┴ └─────────────┘ ┴ ┴
src └───┘ └───┘ └────┘ └─────────────┘
typ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └────┘ ┴ └─────────────┘ ┴ ┴
doc └───┘ └───┘ └────┘
319 (λj k, int.sub_nat_nat_elim w y
id ┴ ┴ └──────────────────┘ ┴ ┴
src └──────────────────┘
typ ┴ ┴ └──────────────────┘ ┴ ┴
320 (λm n i, sq_le n d (k + j) 1 → sq_le k 1 m d → nonneg ⟨int.of_nat j, i⟩)
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └────┘ └────────┘ ┴ ┴
src └───┘ ┴ └───┘ └────┘ └────────┘
typ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └────┘ └────────┘ ┴ ┴
doc └───┘ └───┘ └────┘
321 (λm n xy zw, trivial)
id ┴ ┴ └┘ └┘ └─────┘
src └─────┘
typ ┴ ┴ └┘ └┘ └─────┘
322 (λm n xy zw, sq_le_cancel zw xy))
id ┴ ┴ └┘ └┘ └──────────┘ └┘ └┘
src └──────────┘
typ ┴ ┴ └┘ └┘ └──────────┘ └┘ └┘
323 (λj k, int.sub_nat_nat_elim w y
id ┴ ┴ └──────────────────┘ ┴ ┴
src └──────────────────┘
typ ┴ ┴ └──────────────────┘ ┴ ┴
324 (λm n i, sq_le n d k 1 → sq_le (k + j + 1) 1 m d → nonneg ⟨-[1+ j], i⟩)
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └──┘ ┴┴ ┴
src └───┘ └───┘ ┴ ┴ └────┘ └──┘ ┴
typ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └──┘ ┴┴ ┴
doc └───┘ └───┘ └────┘
325 (λm n xy zw, sq_le_cancel xy zw)
id ┴ ┴ └┘ └┘ └──────────┘ └┘ └┘
src └──────────┘
typ ┴ ┴ └┘ └┘ └──────────┘ └┘ └┘
326 (λm n xy zw, let t := nat.le_trans zw (sq_le_of_le (nat.le_add_right n (m+1)) (le_refl _) xy) in
id ┴ ┴ └┘ └┘ ┴ └──────────┘ └┘ └─────────┘ └──────────────┘ ┴ ┴┴ └─────┘ └┘
src └──────────┘ └─────────┘ └──────────────┘ ┴ └─────┘
typ ┴ ┴ └┘ └┘ ┴ └──────────┘ └┘ └─────────┘ └──────────────┘ ┴ ┴┴ └─────┘ └┘
327 have k + j + 1 ≤ k, from nat.mul_self_le_mul_self_iff.2 (by repeat{rw one_mul at t}; exact t),
id ┴ ┴ ┴ ┴ ┴ ┴ └──────────────────────────┘┴ └─────┘ ┴
src ┴ ┴ ┴ └──────────────────────────┘┴ └─────┘└─┘└─────┘└───┘┴ └────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────────────────┘┴ └─────┘└─┘└─────┘└───┘┴ └────┘┴
doc └─────┘└─┘ └───┘┴ └────┘
txt └─────┘└─┘ └───┘┴ └────┘
par └─────┘└─┘ └───┘┴ └────┘
pid └──┘ └────┘ ┴
st └─────────────────────┘└┘└──────┘
328 absurd this (not_le_of_gt $ nat.succ_le_succ $ nat.le_add_right _ _))) (nonnegg_pos_neg.1 xy) (nonnegg_neg_pos.1 zw),
id └────┘ └──┘ └──────────┘ └──────────────┘ └──────────────┘ └─────────────┘┴ └┘ └─────────────┘┴ └┘
src └────┘ └──────────┘ └──────────────┘ └──────────────┘ └─────────────┘┴ └─────────────┘┴
typ └────┘ └──┘ └──────────┘ └──────────────┘ └──────────────┘ └─────────────┘┴ └┘ └─────────────┘┴ └┘
329 show nonneg ⟨_, _⟩, by rw [neg_add_eq_sub]; rwa [int.sub_nat_nat_eq_coe,int.sub_nat_nat_eq_coe] at this
id └────┘ └────────────┘ └────────────────────┘ └────────────────────┘
src └────┘ └──┘└────────────┘┴ └───┘└────────────────────┘┴└────────────────────┘└─────────
typ └────┘ └──┘└────────────┘┴ └───┘└────────────────────┘┴└────────────────────┘└─────────
doc └────┘ └──┘ ┴ └───┘ ┴ └─────────
txt └──┘ ┴ └───┘ ┴ └─────────
par └──┘ ┴ └───┘ ┴ └─────────
pid └┘ ┴ └┘ ┴ ┴└──────┘└
st └─────────────────┘┴└─────┘└────────────────────┘└─────────────────────┘┴└────────
330
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
331 theorem nonneg_add {a b : ℤ√d} (ha : nonneg a) (hb : nonneg b) : nonneg (a + b) :=
id └┘┴ └────┘ ┴ └────┘ ┴ └────┘ ┴ ┴ ┴
src ─┘ └┘ └────┘ └────┘ └────┘ ┴
typ ─┘ └┘┴ └────┘ ┴ └────┘ ┴ └────┘ ┴ ┴ ┴
doc ─┘ └┘ └────┘ └────┘ └────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
332 begin
st └─────
333 rcases nonneg_cases ha with ⟨x, y, rfl|rfl|rfl⟩;
id └──────────┘ └┘
src └─────┘└──────────┘┴ └───────────────────────┘
typ └─────┘└──────────┘┴└┘└───────────────────────┘
doc └─────┘ ┴ └───────────────────────┘
txt └─────┘ ┴ └───────────────────────┘
par └─────┘ ┴ └───────────────────────┘
pid ┴ ┴ └───────────────────────┘
st ─────────────────────────────────────────────────────
334 rcases nonneg_cases hb with ⟨z, w, rfl|rfl|rfl⟩; dsimp [add, nonneg] at ha hb ⊢,
id └──────────┘ └┘ └─┘ └────┘
src └─────┘└──────────┘┴ └───────────────────────┘ └─────┘└─┘└┘└────┘└──────────┘
typ └─────┘└──────────┘┴└┘└───────────────────────┘ └─────┘└─┘└┘└────┘└──────────┘
doc └─────┘ ┴ └───────────────────────┘ └─────┘└─┘└┘└────┘└──────────┘
txt └─────┘ ┴ └───────────────────────┘ └─────┘ └┘ └──────────┘
par └─────┘ ┴ └───────────────────────┘ └─────┘ └┘ └──────────┘
pid ┴ ┴ └───────────────────────┘ ┴┴ └┘ ┴┴└────────┘
st ──────────────────────────────────────────────────────────────────────────────────┘└─
335 { trivial },
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ─────┘└──────┘└┘└
336 { refine nonnegg_cases_right (λi h, sq_le_of_le _ _ (nonnegg_pos_neg.1 hb)),
id └─────────────────┘ └─────────┘ └─────────────┘ └┘
src └─────┘└─────────────────┘┴ └───┘└─────────┘└───┘ └─────────────┘└─┘ └┘
typ └─────┘└─────────────────┘┴ └───┘└─────────┘└───┘ └─────────────┘└─┘└┘└┘
doc └─────┘ ┴ └───┘ └───┘ └─┘ └┘
txt └─────┘ ┴ └───┘ └───┘ └─┘ └┘
par └─────┘ ┴ └───┘ └───┘ └─┘ └┘
pid ┴ ┴ └───┘ └───┘ └─┘ └┘
st ─────┘└───────────────────────────────────────────────────────────────────────┘└─
337 { exact int.coe_nat_le.1 (le_of_neg_le_neg (@int.le.intro _ _ y (by simp *))) },
id └────────────┘ └──────────────┘ └──────────┘ ┴
src └────┘└────────────┘└─┘ └──────────────┘┴ └──────────┘└───┘ ┴ ┴└────┘└──┘
typ └────┘└────────────┘└─┘ └──────────────┘┴ └──────────┘└───┘┴┴ ┴└────┘└──┘
doc └────┘ └─┘ ┴ └───┘ ┴ ┴└────┘└──┘
txt └────┘ └─┘ ┴ └───┘ ┴ ┴└────┘└──┘
par └────┘ └─┘ ┴ └───┘ ┴ ┴└────┘└──┘
pid ┴ └─┘ ┴ └───┘ ┴ └────────┘┴
st ───────┘└───────────────────────────────────────────────────────────────┘└─────┘└──┘└┘└
338 { apply nat.le_add_left } },
id └─────────────┘
src └────┘└─────────────┘┴
typ └────┘└─────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────────┘└──┘└
339 { refine nonnegg_cases_left (λi h, sq_le_of_le _ _ (nonnegg_neg_pos.1 hb)),
id └────────────────┘ └─────────┘ └─────────────┘ └┘
src └─────┘└────────────────┘┴ └───┘└─────────┘└───┘ └─────────────┘└─┘ └┘
typ └─────┘└────────────────┘┴ └───┘└─────────┘└───┘ └─────────────┘└─┘└┘└┘
doc └─────┘ ┴ └───┘ └───┘ └─┘ └┘
txt └─────┘ ┴ └───┘ └───┘ └─┘ └┘
par └─────┘ ┴ └───┘ └───┘ └─┘ └┘
pid ┴ ┴ └───┘ └───┘ └─┘ └┘
st ─────┘└──────────────────────────────────────────────────────────────────────┘└─
340 { exact int.coe_nat_le.1 (le_of_neg_le_neg (@int.le.intro _ _ x (by simp *))) },
id └────────────┘ └──────────────┘ └──────────┘ ┴
src └────┘└────────────┘└─┘ └──────────────┘┴ └──────────┘└───┘ ┴ ┴└────┘└──┘
typ └────┘└────────────┘└─┘ └──────────────┘┴ └──────────┘└───┘┴┴ ┴└────┘└──┘
doc └────┘ └─┘ ┴ └───┘ ┴ ┴└────┘└──┘
txt └────┘ └─┘ ┴ └───┘ ┴ ┴└────┘└──┘
par └────┘ └─┘ ┴ └───┘ ┴ ┴└────┘└──┘
pid ┴ └─┘ ┴ └───┘ ┴ └────────┘┴
st ───────┘└───────────────────────────────────────────────────────────────┘└─────┘└──┘└┘└
341 { apply nat.le_add_left } },
id └─────────────┘
src └────┘└─────────────┘┴
typ └────┘└─────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────────┘└──┘└
342 { refine nonnegg_cases_right (λi h, sq_le_of_le _ _ (nonnegg_pos_neg.1 ha)),
id └─────────────────┘ └─────────┘ └─────────────┘ └┘
src └─────┘└─────────────────┘┴ └───┘└─────────┘└───┘ └─────────────┘└─┘ └┘
typ └─────┘└─────────────────┘┴ └───┘└─────────┘└───┘ └─────────────┘└─┘└┘└┘
doc └─────┘ ┴ └───┘ └───┘ └─┘ └┘
txt └─────┘ ┴ └───┘ └───┘ └─┘ └┘
par └─────┘ ┴ └───┘ └───┘ └─┘ └┘
pid ┴ ┴ └───┘ └───┘ └─┘ └┘
st ─────┘└───────────────────────────────────────────────────────────────────────┘└─
343 { exact int.coe_nat_le.1 (le_of_neg_le_neg (@int.le.intro _ _ w (by simp *))) },
id └────────────┘ └──────────────┘ └──────────┘ ┴
src └────┘└────────────┘└─┘ └──────────────┘┴ └──────────┘└───┘ ┴ ┴└────┘└──┘
typ └────┘└────────────┘└─┘ └──────────────┘┴ └──────────┘└───┘┴┴ ┴└────┘└──┘
doc └────┘ └─┘ ┴ └───┘ ┴ ┴└────┘└──┘
txt └────┘ └─┘ ┴ └───┘ ┴ ┴└────┘└──┘
par └────┘ └─┘ ┴ └───┘ ┴ ┴└────┘└──┘
pid ┴ └─┘ ┴ └───┘ ┴ └────────┘┴
st ───────┘└───────────────────────────────────────────────────────────────┘└─────┘└──┘└┘└
344 { apply nat.le_add_right } },
id └──────────────┘
src └────┘└──────────────┘┴
typ └────┘└──────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────┘└──┘└
345 { simpa using nonnegg_pos_neg.2 (sq_le_add (nonnegg_pos_neg.1 ha) (nonnegg_pos_neg.1 hb)) },
id └───────┘ └┘ └─────────────┘ └┘
src └──────────┘ └─┘ └───────┘┴ └─┘ └┘ └─────────────┘└─┘ └─┘
typ └──────────┘ └─┘ └───────┘┴ └─┘└┘└┘ └─────────────┘└─┘└┘└─┘
doc └──────────┘ └─┘ ┴ └─┘ └┘ └─┘ └─┘
txt └──────────┘ └─┘ ┴ └─┘ └┘ └─┘ └─┘
par └──────────┘ └─┘ ┴ └─┘ └┘ └─┘ └─┘
pid ┴└────┘ └─┘ ┴ └─┘ └┘ └─┘ └┘┴
st ─────┘└──────────────────────────────────────────────────────────────────────────────────────┘└┘└
346 { exact nonneg_add_lem ha hb },
id └────────────┘ └┘ └┘
src └────┘└────────────┘┴ ┴ ┴
typ └────┘└────────────┘┴└┘┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────┘└─────────────────────────┘└┘└
347 { refine nonnegg_cases_left (λi h, sq_le_of_le _ _ (nonnegg_neg_pos.1 ha)),
id └────────────────┘ └─────────┘ └─────────────┘ └┘
src └─────┘└────────────────┘┴ └───┘└─────────┘└───┘ └─────────────┘└─┘ └┘
typ └─────┘└────────────────┘┴ └───┘└─────────┘└───┘ └─────────────┘└─┘└┘└┘
doc └─────┘ ┴ └───┘ └───┘ └─┘ └┘
txt └─────┘ ┴ └───┘ └───┘ └─┘ └┘
par └─────┘ ┴ └───┘ └───┘ └─┘ └┘
pid ┴ ┴ └───┘ └───┘ └─┘ └┘
st ─────┘└──────────────────────────────────────────────────────────────────────┘└─
348 { exact int.coe_nat_le.1 (le_of_neg_le_neg (@int.le.intro _ _ z (by simp *))) },
id └────────────┘ └──────────────┘ └──────────┘ ┴
src └────┘└────────────┘└─┘ └──────────────┘┴ └──────────┘└───┘ ┴ ┴└────┘└──┘
typ └────┘└────────────┘└─┘ └──────────────┘┴ └──────────┘└───┘┴┴ ┴└────┘└──┘
doc └────┘ └─┘ ┴ └───┘ ┴ ┴└────┘└──┘
txt └────┘ └─┘ ┴ └───┘ ┴ ┴└────┘└──┘
par └────┘ └─┘ ┴ └───┘ ┴ ┴└────┘└──┘
pid ┴ └─┘ ┴ └───┘ ┴ └────────┘┴
st ───────┘└───────────────────────────────────────────────────────────────┘└─────┘└──┘└┘└
349 { apply nat.le_add_right } },
id └──────────────┘
src └────┘└──────────────┘┴
typ └────┘└──────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────┘└──┘└
350 { rw [add_comm, add_comm ↑y], exact nonneg_add_lem hb ha },
id └──────┘ └──────┘ ┴┴ └────────────┘ └┘ └┘
src └──┘└──────┘└┘└──────┘┴┴ ┴ └────┘└────────────┘┴ ┴ ┴
typ └──┘└──────┘└┘└──────┘┴┴┴┴ └────┘└────────────┘┴└┘┴└┘┴
doc └──┘ └┘ ┴ ┴ └────┘ ┴ ┴ ┴
txt └──┘ └┘ ┴ ┴ └────┘ ┴ ┴ ┴
par └──┘ └┘ ┴ ┴ └────┘ ┴ ┴ ┴
pid └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
st ─────┘└──────────┘└───────────┘└────────────────────────────┘└┘└
351 { simpa using nonnegg_neg_pos.2 (sq_le_add (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb)) },
id └───────┘ └┘ └─────────────┘ └┘
src └──────────┘ └─┘ └───────┘┴ └─┘ └┘ └─────────────┘└─┘ └─┘
typ └──────────┘ └─┘ └───────┘┴ └─┘└┘└┘ └─────────────┘└─┘└┘└─┘
doc └──────────┘ └─┘ ┴ └─┘ └┘ └─┘ └─┘
txt └──────────┘ └─┘ ┴ └─┘ └┘ └─┘ └─┘
par └──────────┘ └─┘ ┴ └─┘ └┘ └─┘ └─┘
pid ┴└────┘ └─┘ ┴ └─┘ └┘ └─┘ └┘┴
st ─────────────────────────────────────────────────────────────────────────────────────────────┘└──
352 end
st ────┘
353
354 theorem le_refl (a : ℤ√d) : a ≤ a := show nonneg (a - a), by simp
id └┘┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └┘ ┴ └────┘ ┴ └────
typ └┘┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────
doc └┘ └────┘ └────
txt └────
par └────
pid └
st └─────
355
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
356 protected theorem le_trans {a b c : ℤ√d} (ab : a ≤ b) (bc : b ≤ c) : a ≤ c :=
id └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ─┘ └┘ ┴ ┴ ┴
typ ─┘ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ─┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
357 have nonneg (b - a + (c - b)), from nonneg_add ab bc,
id └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ └┘ └┘
src └────┘ ┴ ┴ ┴ └────────┘
typ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ └┘ └┘
doc └────┘
358 by simpa
src └─────
typ └─────
doc └─────
txt └─────
par └─────
pid └
st └──────
359
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
360 theorem nonneg_iff_zero_le {a : ℤ√d} : nonneg a ↔ 0 ≤ a := show _ ↔ nonneg _, by simp
id └┘┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘
src ─┘ └┘ └────┘ ┴ ┴ ┴ └────┘ └────
typ ─┘ └┘┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ └────
doc ─┘ └┘ └────┘ └────┘ └────
txt ─┘ └────
par ─┘ └────
pid ─┘ └
st ─┘ └─────
361
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
362 theorem le_of_le_le {x y z w : ℤ} (xz : x ≤ z) (yw : y ≤ w) : (⟨x, y⟩ : ℤ√d) ≤ ⟨z, w⟩ :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴ ┴
src ─┘ ┴ ┴ ┴ └┘ ┴
typ ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴ ┴
doc ─┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
363 show nonneg ⟨z - x, w - y⟩, from
id └────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ ┴
typ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────┘
364 match z - x, w - y, int.le.dest_sub xz, int.le.dest_sub yw with ._, ._, ⟨a, rfl⟩, ⟨b, rfl⟩ := trivial end
id ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘ └┘ └─────────────┘ └┘ └─┘ └─────┘
src ┴ ┴ └─────────────┘ └─────────────┘ └─┘ └─────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘ └┘ └─────────────┘ └┘ └─┘ └─────┘
365
366 theorem le_arch (a : ℤ√d) : ∃n : ℕ, a ≤ n :=
id └┘┴ ┴ ┴┴ ┴ ┴ ┴
src └┘ ┴ ┴┴ ┴
typ └┘┴ ┴ ┴┴ ┴ ┴ ┴
doc └┘
367 let ⟨x, y, (h : a ≤ ⟨x, y⟩)⟩ := show ∃x y : ℕ, nonneg (⟨x, y⟩ + -a), from match -a with
id └─┘ ┴ ┴ ┴ ┴┴ └────┘ ┴ ┴ ┴ ┴┴ ┴┴
src ┴ ┴ ┴┴ └────┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴┴ └────┘ ┴ ┴ ┴ ┴┴ ┴┴
doc └────┘
368 | ⟨int.of_nat x, int.of_nat y⟩ := ⟨0, 0, trivial⟩
id └────────┘ └─────┘
src └────────┘ └─────┘
typ └────────┘ └─────┘
369 | ⟨int.of_nat x, -[1+ y]⟩ := ⟨0, y+1, by simp [int.neg_succ_of_nat_coe]⟩
id └────────┘ └──┘ ┴┴ ┴ └─────────────────────┘
src └────────┘ └──┘ ┴ ┴ └────┘└─────────────────────┘┴
typ └────────┘ └──┘ ┴┴ ┴ └────┘└─────────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────────────────────────┘
370 | ⟨-[1+ x], int.of_nat y⟩ := ⟨x+1, 0, by simp [int.neg_succ_of_nat_coe]⟩
id └──┘ ┴┴ └────────┘ ┴ └─────────────────────┘
src └──┘ ┴ └────────┘ ┴ └────┘└─────────────────────┘┴
typ └──┘ ┴┴ └────────┘ ┴ └────┘└─────────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────────────────────────┘
371 | ⟨-[1+ x], -[1+ y]⟩ := ⟨x+1, y+1, by simp [int.neg_succ_of_nat_coe]⟩
id └──┘ ┴┴ └──┘ ┴┴ ┴ ┴ └─────────────────────┘
src └──┘ ┴ └──┘ ┴ ┴ ┴ └────┘└─────────────────────┘┴
typ └──┘ ┴┴ └──┘ ┴┴ ┴ ┴ └────┘└─────────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────────────────────────┘
372 end in begin
st └─────
373 refine ⟨x + d*y, zsqrtd.le_trans h _⟩,
id ┴ ┴ ┴┴┴ ┴
src └─────┘ ┴┴┴ ┴ └┘ ┴ └─┘
typ └─────┘ ┴┴┴┴┴┴┴└┘ ┴┴└─┘
doc └─────┘ ┴ ┴ └┘ ┴ └─┘
txt └─────┘ ┴ ┴ └┘ ┴ └─┘
par └─────┘ ┴ ┴ └┘ ┴ └─┘
pid ┴ ┴ ┴ └┘ ┴ └─┘
st ────────────────────────────────────────┘└─
374 rw [← int.cast_coe_nat, ← of_int_eq_coe],
id └──────────────┘ └───────────┘
src └────┘└──────────────┘└──┘└───────────┘┴
typ └────┘└──────────────┘└──┘└───────────┘┴
doc └────┘ └──┘ ┴
txt └────┘ └──┘ ┴
par └────┘ └──┘ ┴
pid └──┘ └──┘ ┴
st ─────────────────────────┘└───────────────┘└──
375 change nonneg ⟨(↑x + d*y) - ↑x, 0-↑y⟩,
id └────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘└────┘┴ ┴ ┴ ┴ └┘┴┴ └─┘ ┴
typ └─────┘└────┘┴ ┴ ┴ ┴┴ └┘┴┴ ┴└─┘ ┴┴
doc └─────┘└────┘┴ ┴ ┴ └┘ ┴ └─┘ ┴
txt └─────┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴
par └─────┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴
pid ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴
st ────────────────────────────────────────┘└─
376 cases y with y,
id ┴
src └────┘ └─────┘
typ └────┘┴└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └─────┘
st ─────────────────┘└─
377 { simp },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ─────┘└───┘└┘└
378 have h : ∀y, sq_le y d (d * y) 1 := λ y,
id └───┘ ┴
src └───────┘ ┴ ┴└───┘┴ ┴ ┴ ┴ ┴ └─────┘ └───
typ └───────┘ ┴ ┴└───┘┴ ┴ ┴ ┴┴ ┴ └─────┘ └───
doc └───────┘ ┴ ┴└───┘┴ ┴ ┴ ┴ ┴ └─────┘ └───
txt └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └───
par └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └───
pid └────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘└───┘ └───
st ─────────────────────────────────────────────
379 by simpa [sq_le, mul_comm, mul_left_comm] using
id └───┘ └──────┘ └───────────┘
src ─────┘ ┴└─────┘└───┘└┘└──────┘└┘└───────────┘└───────
typ ─────┘ ┴└─────┘└───┘└┘└──────┘└┘└───────────┘└───────
doc ─────┘ ┴└─────┘└───┘└┘ └┘ └───────
txt ─────┘ ┴└─────┘ └┘ └┘ └───────
par ─────┘ ┴└─────┘ └┘ └┘ └───────
pid ─────┘ └──────┘ └┘ └┘ └───────
st ───────┘└─────────────────────────────────────────────
380 nat.mul_le_mul_right (y * y) (nat.le_mul_self d),
id └──────────────────┘ ┴ └─────────────┘ ┴
src ────────┘└──────────────────┘┴ ┴ ┴ └┘ └─────────────┘┴ ┴
typ ────────┘└──────────────────┘┴ ┴ ┴┴└┘ └─────────────┘┴┴┴
doc ────────┘ ┴ ┴ ┴ └┘ ┴ ┴
txt ────────┘ ┴ ┴ ┴ └┘ ┴ ┴
par ────────┘ ┴ ┴ ┴ └┘ ┴ ┴
pid ────────┘ ┴ ┴ ┴ └┘ ┴ ┴
st ────────────────────────────────────────────────────────┘└─
381 rw [show (x:ℤ) + d * nat.succ y - x = d * nat.succ y, by simp],
id ┴ ┴ ┴ └──────┘ ┴
src └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴└──────┘┴ └───┘└──┘┴
typ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴┴┴┴┴┴ ┴└──────┘┴┴└───┘└──┘┴
doc └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘└──┘┴
txt └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘└──┘┴
par └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘└──┘┴
pid └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘
st ───────────────────────────────────────────────────────────┘└───┘└──
382 exact h (y+1)
id ┴ ┴
src └────┘ ┴ └──
typ └────┘┴┴ ┴ └──
doc └────┘ ┴ └──
txt └────┘ ┴ └──
par └────┘ ┴ └──
pid ┴ ┴ └┘└
st ──────────────────
383 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
384
385 protected theorem nonneg_total : Π (a : ℤ√d), nonneg a ∨ nonneg (-a)
id ┴ └┘┴ └────┘ ┴ ┴ └────┘ ┴┴
src └┘ └────┘ ┴ └────┘ ┴
typ ┴ └┘┴ └────┘ ┴ ┴ └────┘ ┴┴
doc └┘ └────┘ └────┘
386 | ⟨(x : ℕ), (y : ℕ)⟩ := or.inl trivial
id ┴ ┴ └────┘ └─────┘
src ┴ ┴ └────┘ └─────┘
typ ┴ ┴ └────┘ └─────┘
387 | ⟨-[1+ x], -[1+ y]⟩ := or.inr trivial
id └──┘ ┴ └──┘ ┴ └────┘ └─────┘
src └──┘ ┴ └──┘ ┴ └────┘ └─────┘
typ └──┘ ┴ └──┘ ┴ └────┘ └─────┘
388 | ⟨0, -[1+ y]⟩ := or.inr trivial
id └──┘ ┴ └────┘ └─────┘
src └──┘ ┴ └────┘ └─────┘
typ └──┘ ┴ └────┘ └─────┘
389 | ⟨-[1+ x], 0⟩ := or.inr trivial
id └──┘ ┴ └────┘ └─────┘
src └──┘ ┴ └────┘ └─────┘
typ └──┘ ┴ └────┘ └─────┘
390 | ⟨(x+1:ℕ), -[1+ y]⟩ := nat.le_total
id ┴ ┴ └──┘ ┴ └──────────┘
src ┴ ┴ └──┘ ┴ └──────────┘
typ ┴ ┴ └──┘ ┴ └──────────┘
391 | ⟨-[1+ x], (y+1:ℕ)⟩ := nat.le_total
id └──┘ ┴ ┴ ┴ └──────────┘
src └──┘ ┴ ┴ ┴ └──────────┘
typ └──┘ ┴ ┴ ┴ └──────────┘
392
393 protected theorem le_total (a b : ℤ√d) : a ≤ b ∨ b ≤ a :=
id └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ ┴
typ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
394 let t := nonneg_total (b - a) in by rw [show -(b-a) = a-b, from neg_sub b a] at t; exact t
id ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴
src └──────────┘ ┴ └──┘ ┴┴ ┴ └┘┴┴ └─────┘└─────┘┴ ┴ └────┘ └────┘ └
typ ┴ └──────────┘ ┴ ┴ ┴ └──┘ ┴┴ ┴ └┘┴┴ └─────┘└─────┘┴┴┴┴└────┘ └────┘┴└
doc └──┘ ┴ └┘ ┴ └─────┘ ┴ ┴ └────┘ └────┘ └
txt └──┘ ┴ └┘ ┴ └─────┘ ┴ ┴ └────┘ └────┘ └
par └──┘ ┴ └┘ ┴ └─────┘ ┴ ┴ └────┘ └────┘ └
pid └┘ ┴ └┘ ┴ └─────┘ ┴ ┴ ┴└───┘ ┴ └
st └──────────────────────────────────────┘┴└──────────────
395
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
396 instance : preorder ℤ√d :=
id └──────┘ └┘┴
src ─┘ └──────┘ └┘
typ ─┘ └──────┘ └┘┴
doc ─┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
397 { le := zsqrtd.le,
id └───────┘
src └───────┘
typ └───────┘
398 le_refl := zsqrtd.le_refl,
id └────────────┘
src └────────────┘
typ └────────────┘
399 le_trans := @zsqrtd.le_trans,
id └─────────────┘
src └─────────────┘
typ └─────────────┘
400 lt := zsqrtd.lt,
id └───────┘
src └───────┘
typ └───────┘
401 lt_iff_le_not_le := λ a b,
id ┴ ┴
typ ┴ ┴
402 (and_iff_right_of_imp (zsqrtd.le_total _ _).resolve_left).symm }
id └──────────────────┘ └─────────────┘ └──────────┘ └──┘
src └──────────────────┘ └─────────────┘ └──────────┘ └──┘
typ └──────────────────┘ └─────────────┘ └──────────┘ └──┘
403
404 protected theorem add_le_add_left (a b : ℤ√d) (ab : a ≤ b) (c : ℤ√d) : c + a ≤ c + b :=
id └┘┴ ┴ ┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └┘ ┴ ┴ ┴
typ └┘┴ ┴ ┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘
405 show nonneg _, by rw add_sub_add_left_eq_sub; exact ab
id └────┘ └─────────────────────┘ └┘
src └────┘ └─┘└─────────────────────┘ └────┘ └
typ └────┘ └─┘└─────────────────────┘ └────┘└┘└
doc └────┘ └─┘ └────┘ └
txt └─┘ └────┘ └
par └─┘ └────┘ └
pid ┴ ┴ └
st └─────────────────────────────────────
406
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
407 protected theorem le_of_add_le_add_left (a b c : ℤ√d) (h : c + a ≤ c + b) : a ≤ b :=
id └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ─┘ └┘ ┴ ┴ ┴ ┴
typ ─┘ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ─┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
408 by simpa using zsqrtd.add_le_add_left _ _ h (-c)
id ┴ ┴┴
src └──────────┘ └───┘ ┴ ┴ └─
typ └──────────┘ └───┘┴┴ ┴┴└─
doc └──────────┘ └───┘ ┴ └─
txt └──────────┘ └───┘ ┴ └─
par └──────────┘ └───┘ ┴ └─
pid ┴└────┘ └───┘ ┴ ┴└
st └──────────────────────────────────────────────
409
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
410 protected theorem add_lt_add_left (a b : ℤ√d) (h : a < b) (c) : c + a < c + b :=
id └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ─┘ └┘ ┴ ┴ ┴ ┴
typ ─┘ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ─┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
411 λ h', h (zsqrtd.le_of_add_le_add_left _ _ _ h')
id └┘ ┴ └──────────────────────────┘ └┘
src └──────────────────────────┘
typ └┘ ┴ └──────────────────────────┘ └┘
412
413 theorem nonneg_smul {a : ℤ√d} {n : ℕ} (ha : nonneg a) : nonneg (n * a) :=
id └┘┴ ┴ └────┘ ┴ └────┘ ┴ ┴ ┴
src └┘ ┴ └────┘ └────┘ ┴
typ └┘┴ ┴ └────┘ ┴ └────┘ ┴ ┴ ┴
doc └┘ └────┘ └────┘
414 by rw ← int.cast_coe_nat; exact match a, nonneg_cases ha, ha with
id └──────────────┘ ┴ └──────────┘ └┘
src └───┘└──────────────┘ └────┘ ┴ └┘└──────────┘┴ └┘ └─────
typ └───┘└──────────────┘ └────┘ ┴┴└┘└──────────┘┴ └┘└┘└─────
doc └───┘ └────┘ ┴ └┘ ┴ └┘ └─────
txt └───┘ └────┘ ┴ └┘ ┴ └┘ └─────
par └───┘ └────┘ ┴ └┘ ┴ └┘ └─────
pid └─┘ ┴ ┴ └┘ ┴ └┘ └─────
st └───────────────────────────────────────────────────────────────
415 | ._, ⟨x, y, or.inl rfl⟩, ha := by rw smul_val; trivial
id └────┘ └─┘ └──────┘
src ───┘ └┘ └┘ └┘└────┘┴└─┘└──────────┘ └──┘ ┴└─┘└──────┘└┘└───────
typ ───┘ └┘ └┘ └┘└────┘┴└─┘└──────────┘ └──┘ ┴└─┘└──────┘└┘└───────
doc ───┘ └┘ └┘ └┘ ┴ └──────────┘ └──┘ ┴└─┘ └┘└───────
txt ───┘ └┘ └┘ └┘ ┴ └──────────┘ └──┘ ┴└─┘ └┘└───────
par ───┘ └┘ └┘ └┘ ┴ └──────────┘ └──┘ ┴└─┘ └┘└───────
pid ───┘ └┘ └┘ └┘ ┴ └──────────┘ └──┘ └──┘ └─────────
st ────────────────────────────────────────────┘└─────────────────────
416 | ._, ⟨x, y, or.inr $ or.inl rfl⟩, ha := by rw smul_val; simpa using
id └────┘ └──────┘
src ─┘└┘ └┘ └┘ └┘└────┘┴ ┴ ┴ └─┘ └──┘ ┴└─┘└──────┘└┘└───────────
typ ─┘└┘ └┘ └┘ └┘└────┘┴ ┴ ┴ └─┘ └──┘ ┴└─┘└──────┘└┘└───────────
doc ─┘└┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└─┘ └┘└───────────
txt ─┘└┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└─┘ └┘└───────────
par ─┘└┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└─┘ └┘└───────────
pid ───┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ └──┘ └─────────────
st ─┘└─────────────────────────────────────────┘└─────────────────────────
417 nonnegg_pos_neg.2 (sq_le_smul n $ nonnegg_pos_neg.1 ha)
id └────────┘ ┴ └─────────────┘ └┘
src ───┘ └─┘ └────────┘┴ ┴ ┴└─────────────┘└─┘ └─
typ ───┘ └─┘ └────────┘┴┴┴ ┴└─────────────┘└─┘└┘└─
doc ───┘ └─┘ ┴ ┴ ┴ └─┘ └─
txt ───┘ └─┘ ┴ ┴ ┴ └─┘ └─
par ───┘ └─┘ ┴ ┴ ┴ └─┘ └─
pid ───┘ └─┘ ┴ ┴ ┴ └─┘ └─
st ────────────────────────────────────────────────────────────
418 | ._, ⟨x, y, or.inr $ or.inr rfl⟩, ha := by rw smul_val; simpa using
id └──────┘
src ─┘└┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└─┘└──────┘└┘└───────────
typ ─┘└┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└─┘└──────┘└┘└───────────
doc ─┘└┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└─┘ └┘└───────────
txt ─┘└┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└─┘ └┘└───────────
par ─┘└┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└─┘ └┘└───────────
pid ───┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ └──┘ └─────────────
st ─┘└─────────────────────────────────────────┘└─────────────────────────
419 nonnegg_neg_pos.2 (sq_le_smul n $ nonnegg_neg_pos.1 ha)
id └────────┘ ┴ └─────────────┘ └┘
src ───┘ └─┘ └────────┘┴ ┴ ┴└─────────────┘└─┘ └─
typ ───┘ └─┘ └────────┘┴┴┴ ┴└─────────────┘└─┘└┘└─
doc ───┘ └─┘ ┴ ┴ ┴ └─┘ └─
txt ───┘ └─┘ ┴ ┴ ┴ └─┘ └─
par ───┘ └─┘ ┴ ┴ ┴ └─┘ └─
pid ───┘ └─┘ ┴ ┴ ┴ └─┘ └─
st ────────────────────────────────────────────────────────────
420 end
src ─┘└───
typ ─┘└───
doc ─┘└───
txt ─┘└───
par ─┘└───
pid ────┘└
st ─┘└───
421
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
422 theorem nonneg_muld {a : ℤ√d} (ha : nonneg a) : nonneg (sqrtd * a) :=
id └┘┴ └────┘ ┴ └────┘ └───┘ ┴ ┴
src ─┘ └┘ └────┘ └────┘ └───┘ ┴
typ ─┘ └┘┴ └────┘ ┴ └────┘ └───┘ ┴ ┴
doc ─┘ └┘ └────┘ └────┘ └───┘
txt ─┘
par ─┘
pid ─┘
st ─┘
423 by refine match a, nonneg_cases ha, ha with
id ┴ └──────────┘ └┘
src └─────┘ ┴ └┘└──────────┘┴ └┘ └─────
typ └─────┘ ┴┴└┘└──────────┘┴ └┘└┘└─────
doc └─────┘ ┴ └┘ ┴ └┘ └─────
txt └─────┘ ┴ └┘ ┴ └┘ └─────
par └─────┘ ┴ └┘ ┴ └┘ └─────
pid ┴ ┴ └┘ ┴ └┘ └─────
st └─────────────────────────────────────────
424 | ._, ⟨x, y, or.inl rfl⟩, ha := trivial
id └────┘ └─┘ └─────┘
src ───┘ └┘ └┘ └┘└────┘┴└─┘└──────────┘ └──┘└─────┘└
typ ───┘ └┘ └┘ └┘└────┘┴└─┘└──────────┘ └──┘└─────┘└
doc ───┘ └┘ └┘ └┘ ┴ └──────────┘ └──┘ └
txt ───┘ └┘ └┘ └┘ ┴ └──────────┘ └──┘ └
par ───┘ └┘ └┘ └┘ ┴ └──────────┘ └──┘ └
pid ───┘ └┘ └┘ └┘ ┴ └──────────┘ └──┘ └
st ───────────────────────────────────────────────────
425 | ._, ⟨x, y, or.inr $ or.inl rfl⟩, ha := by simp; apply nonnegg_neg_pos.2;
id └────┘ └─────────────┘
src ───┘ └┘ └┘ └┘└────┘┴ ┴ ┴ └─┘ └──┘ ┴└──┘└┘└────┘└─────────────┘└┘└─
typ ───┘ └┘ └┘ └┘└────┘┴ ┴ ┴ └─┘ └──┘ ┴└──┘└──────┘└─────────────┘└───
doc ───┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└──┘└┘└────┘ └┘└─
txt ───┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└──┘└┘└────┘ └┘└─
par ───┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└──┘└──────┘ └───
pid ───┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ └───────────┘ └───
st ────────────────────────────────────────────┘└───────────────────────────────
426 simpa [sq_le, mul_comm, mul_left_comm] using
id └───┘ └──────┘ └───────────┘
src ───┘└─────┘└───┘└┘└──────┘└┘└───────────┘└───────
typ ───┘└─────┘└───┘└┘└──────┘└┘└───────────┘└───────
doc ───┘└─────┘└───┘└┘ └┘ └───────
txt ───┘└─────┘ └┘ └┘ └───────
par ───┘└─────┘ └┘ └┘ └───────
pid ──────────┘ └┘ └┘ └───────
st ─────────────────────────────────────────────────
427 nat.mul_le_mul_left d (nonnegg_pos_neg.1 ha)
id └─────────────────┘ ┴ └─────────────┘ └┘
src ─────┘└─────────────────┘┴ ┴ └─────────────┘└─┘ └─
typ ─────┘└─────────────────┘┴┴┴ └─────────────┘└─┘└┘└─
doc ─────┘ ┴ ┴ └─┘ └─
txt ─────┘ ┴ ┴ └─┘ └─
par ─────┘ ┴ ┴ └─┘ └─
pid ─────┘ ┴ ┴ └─┘ └─
st ───────────────────────────────────────────────────
428 | ._, ⟨x, y, or.inr $ or.inr rfl⟩, ha := by simp; apply nonnegg_pos_neg.2;
id └─────────────┘
src ─┘└┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└──┘└┘└────┘└─────────────┘└┘└─
typ ─┘└┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└──┘└──────┘└─────────────┘└───
doc ─┘└┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└──┘└┘└────┘ └┘└─
txt ─┘└┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└──┘└┘└────┘ └┘└─
par ─┘└┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴└──┘└──────┘ └───
pid ───┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ └───────────┘ └───
st ─┘└─────────────────────────────────────────┘└───────────────────────────────
429 simpa [sq_le, mul_comm, mul_left_comm] using
id └───┘ └──────┘ └───────────┘
src ───┘└─────┘└───┘└┘└──────┘└┘└───────────┘└───────
typ ───┘└─────┘└───┘└┘└──────┘└┘└───────────┘└───────
doc ───┘└─────┘└───┘└┘ └┘ └───────
txt ───┘└─────┘ └┘ └┘ └───────
par ───┘└─────┘ └┘ └┘ └───────
pid ──────────┘ └┘ └┘ └───────
st ─────────────────────────────────────────────────
430 nat.mul_le_mul_left d (nonnegg_neg_pos.1 ha)
id └─────────────────┘ ┴ └─────────────┘ └┘
src ─────┘└─────────────────┘┴ ┴ └─────────────┘└─┘ └─
typ ─────┘└─────────────────┘┴┴┴ └─────────────┘└─┘└┘└─
doc ─────┘ ┴ ┴ └─┘ └─
txt ─────┘ ┴ ┴ └─┘ └─
par ─────┘ ┴ ┴ └─┘ └─
pid ─────┘ ┴ ┴ └─┘ └─
st ───────────────────────────────────────────────────
431 end
src ─┘└───
typ ─┘└───
doc ─┘└───
txt ─┘└───
par ─┘└───
pid ────┘└
st ─┘└───
432
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
433 theorem nonneg_mul_lem {x y : ℕ} {a : ℤ√d} (ha : nonneg a) : nonneg (⟨x, y⟩ * a) :=
id ┴ └┘┴ └────┘ ┴ └────┘ ┴ ┴ ┴ ┴
src ─┘ ┴ └┘ └────┘ └────┘ ┴
typ ─┘ ┴ └┘┴ └────┘ ┴ └────┘ ┴ ┴ ┴ ┴
doc ─┘ └┘ └────┘ └────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
434 have (⟨x, y⟩ * a : ℤ√d) = x * a + sqrtd * (y * a), by rw [decompose, right_distrib, mul_assoc]; refl,
id ┴ ┴ ┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───────┘ └───────────┘ └───────┘
src ┴ └┘ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘└───────┘└┘└───────────┘└┘└───────┘┴ └──┘
typ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └──┘└───────┘└┘└───────────┘└┘└───────┘┴ └──┘
doc └┘ └───┘ └──┘ └┘ └┘ ┴ └──┘
txt └──┘ └┘ └┘ ┴ └──┘
par └──┘ └┘ └┘ ┴ └──┘
pid └┘ └┘ └┘ ┴
st └────────────┘└─────────────┘└─────────┘┴└────┘
435 by rw this; exact nonneg_add (nonneg_smul ha) (nonneg_muld $ nonneg_smul ha)
id └──┘ └────────┘ └─────────┘ └─────────┘ └┘
src └─┘ └────┘└────────┘┴ ┴ └┘ └─────────┘┴ ┴└─────────┘┴ └─
typ └─┘└──┘ └────┘└────────┘┴ ┴ └┘ └─────────┘┴ ┴└─────────┘┴└┘└─
doc └─┘ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─
txt └─┘ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─
par └─┘ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─
pid ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴└
st └──────────────────────────────────────────────────────────────────────────
436
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
437 theorem nonneg_mul {a b : ℤ√d} (ha : nonneg a) (hb : nonneg b) : nonneg (a * b) :=
id └┘┴ └────┘ ┴ └────┘ ┴ └────┘ ┴ ┴ ┴
src ─┘ └┘ └────┘ └────┘ └────┘ ┴
typ ─┘ └┘┴ └────┘ ┴ └────┘ ┴ └────┘ ┴ ┴ ┴
doc ─┘ └┘ └────┘ └────┘ └────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
438 match a, b, nonneg_cases ha, nonneg_cases hb, ha, hb with
id ┴ ┴ └──────────┘ └┘ └──────────┘ └┘ └┘ └┘
src └──────────┘ └──────────┘
typ ┴ ┴ └──────────┘ └┘ └──────────┘ └┘ └┘ └┘
439 | ._, ._, ⟨x, y, or.inl rfl⟩, ⟨z, w, or.inl rfl⟩, ha, hb := trivial
id └────┘ └─┘ └─────┘
src └────┘ └─┘ └─────┘
typ └────┘ └─┘ └─────┘
440 | ._, ._, ⟨x, y, or.inl rfl⟩, ⟨z, w, or.inr $ or.inr rfl⟩, ha, hb := nonneg_mul_lem hb
id └────┘ └────┘ └─┘ └┘ └────────────┘
src └────┘ └────┘ └─┘ └────────────┘
typ └────┘ └────┘ └─┘ └┘ └────────────┘
441 | ._, ._, ⟨x, y, or.inl rfl⟩, ⟨z, w, or.inr $ or.inl rfl⟩, ha, hb := nonneg_mul_lem hb
id └────┘ └────┘ └─┘ └┘ └────────────┘
src └────┘ └────┘ └─┘ └────────────┘
typ └────┘ └────┘ └─┘ └┘ └────────────┘
442 | ._, ._, ⟨x, y, or.inr $ or.inr rfl⟩, ⟨z, w, or.inl rfl⟩, ha, hb := by rw mul_comm; exact nonneg_mul_lem ha
id └────┘ └────┘ └─┘ └──────┘ └────────────┘ └┘
src └────┘ └────┘ └─┘ └─┘└──────┘ └────┘└────────────┘┴ └
typ └────┘ └────┘ └─┘ └─┘└──────┘ └────┘└────────────┘┴└┘└
doc └─┘ └────┘ ┴ └
txt └─┘ └────┘ ┴ └
par └─┘ └────┘ ┴ └
pid ┴ ┴ ┴ └
st └─────────────────────────────────────
443 | ._, ._, ⟨x, y, or.inr $ or.inl rfl⟩, ⟨z, w, or.inl rfl⟩, ha, hb := by rw mul_comm; exact nonneg_mul_lem ha
id └────┘ └────┘ └─┘ └──────┘ └────────────┘ └┘
src ─┘ └────┘ └────┘ └─┘ └─┘└──────┘ └────┘└────────────┘┴ └
typ ─┘ └────┘ └────┘ └─┘ └─┘└──────┘ └────┘└────────────┘┴└┘└
doc ─┘ └─┘ └────┘ ┴ └
txt ─┘ └─┘ └────┘ ┴ └
par ─┘ └─┘ └────┘ ┴ └
pid ─┘ ┴ ┴ ┴ └
st ─┘ └─────────────────────────────────────
444 | ._, ._, ⟨x, y, or.inr $ or.inr rfl⟩, ⟨z, w, or.inr $ or.inr rfl⟩, ha, hb :=
id └────┘ └─┘
src ─┘ └────┘ └─┘
typ ─┘ └────┘ └─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
445 by rw [calc (⟨-x, y⟩ * ⟨-z, w⟩ : ℤ√d) = ⟨_, _⟩ : rfl
id ┴ ┴ └─┘
src └──┘ ┴ ┴ └┘ └┘┴┴ └┘ └──┘ └┘ ┴ └──────┘└─┘└
typ └──┘ ┴ ┴ └┘ └┘┴┴ └┘ └──┘ └┘ ┴ └──────┘└─┘└
doc └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
txt └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
par └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
pid └┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
st └──────────────────────────────────────────────────
446 ... = ⟨x * z + d * y * w, -(x * w + y * z)⟩ : by simp]; exact
id ┴ ┴ ┴ ┴ ┴ ┴
src ───────────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴└──┘┴ └─────
typ ───────────┘ ┴ ┴ ┴ ┴┴┴┴┴ ┴ ┴ ┴ └┘ ┴┴ ┴┴┴ ┴┴┴ ┴┴└───┘ ┴└──┘┴ └─────
doc ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴└──┘┴ └─────
txt ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴└──┘┴ └─────
par ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴└──┘┴ └─────
pid ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └────┘ └
st ───────────────────────────────────────────────────────┘└───┘┴└───────
447 nonnegg_pos_neg.2 (sq_le_mul.left (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb))
id └─────────────┘ └────────────┘ └┘ └─────────────┘ └┘
src ───┘└─────────────┘└─┘ └────────────┘┴ └─┘ └┘ └─────────────┘└─┘ └──
typ ───┘└─────────────┘└─┘ └────────────┘┴ └─┘└┘└┘ └─────────────┘└─┘└┘└──
doc ───┘ └─┘ ┴ └─┘ └┘ └─┘ └──
txt ───┘ └─┘ ┴ └─┘ └┘ └─┘ └──
par ───┘ └─┘ ┴ └─┘ └┘ └─┘ └──
pid ───┘ └─┘ ┴ └─┘ └┘ └─┘ └┘└
st ─────────────────────────────────────────────────────────────────────────────────────
448 | ._, ._, ⟨x, y, or.inr $ or.inr rfl⟩, ⟨z, w, or.inr $ or.inl rfl⟩, ha, hb :=
id └────┘ └────┘ └─┘
src ─┘ └────┘ └────┘ └─┘
typ ─┘ └────┘ └────┘ └─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
449 by rw [calc (⟨-x, y⟩ * ⟨z, -w⟩ : ℤ√d) = ⟨_, _⟩ : rfl
id └─┘
src └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘└─┘└
typ └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘└─┘└
doc └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
txt └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
par └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
pid └┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
st └──────────────────────────────────────────────────
450 ... = ⟨-(x * z + d * y * w), x * w + y * z⟩ : by simp]; exact
id ┴ ┴ ┴ ┴ ┴
src ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└──┘┴ └─────
typ ───────────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ └─┘┴┴ ┴┴┴ ┴┴┴ ┴┴└──┘ ┴└──┘┴ └─────
doc ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└──┘┴ └─────
txt ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└──┘┴ └─────
par ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└──┘┴ └─────
pid ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └────┘ └
st ───────────────────────────────────────────────────────┘└───┘┴└───────
451 nonnegg_neg_pos.2 (sq_le_mul.right.left (nonnegg_neg_pos.1 ha) (nonnegg_pos_neg.1 hb))
id └──────────────────┘ └─────────────┘ └┘ └─────────────┘ └┘
src ───┘ └─┘ └──────────────────┘┴ └─────────────┘└─┘ └┘ └─────────────┘└─┘ └──
typ ───┘ └─┘ └──────────────────┘┴ └─────────────┘└─┘└┘└┘ └─────────────┘└─┘└┘└──
doc ───┘ └─┘ ┴ └─┘ └┘ └─┘ └──
txt ───┘ └─┘ ┴ └─┘ └┘ └─┘ └──
par ───┘ └─┘ ┴ └─┘ └┘ └─┘ └──
pid ───┘ └─┘ ┴ └─┘ └┘ └─┘ └┘└
st ───────────────────────────────────────────────────────────────────────────────────────────
452 | ._, ._, ⟨x, y, or.inr $ or.inl rfl⟩, ⟨z, w, or.inr $ or.inr rfl⟩, ha, hb :=
id └────┘ └────┘ └─┘
src ─┘ └────┘ └────┘ └─┘
typ ─┘ └────┘ └────┘ └─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
453 by rw [calc (⟨x, -y⟩ * ⟨-z, w⟩ : ℤ√d) = ⟨_, _⟩ : rfl
id └─┘
src └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘└─┘└
typ └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘└─┘└
doc └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
txt └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
par └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
pid └┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
st └──────────────────────────────────────────────────
454 ... = ⟨-(x * z + d * y * w), x * w + y * z⟩ : by simp]; exact
id ┴ ┴ ┴ ┴ ┴
src ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└──┘┴ └─────
typ ───────────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ └─┘┴┴ ┴┴┴ ┴┴┴ ┴┴└──┘ ┴└──┘┴ └─────
doc ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└──┘┴ └─────
txt ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└──┘┴ └─────
par ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└──┘┴ └─────
pid ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └────┘ └
st ───────────────────────────────────────────────────────┘└───┘┴└───────
455 nonnegg_neg_pos.2 (sq_le_mul.right.right.left (nonnegg_pos_neg.1 ha) (nonnegg_neg_pos.1 hb))
id └────────────────────────┘ └─────────────┘ └┘ └─────────────┘ └┘
src ───┘ └─┘ └────────────────────────┘┴ └─────────────┘└─┘ └┘ └─────────────┘└─┘ └──
typ ───┘ └─┘ └────────────────────────┘┴ └─────────────┘└─┘└┘└┘ └─────────────┘└─┘└┘└──
doc ───┘ └─┘ ┴ └─┘ └┘ └─┘ └──
txt ───┘ └─┘ ┴ └─┘ └┘ └─┘ └──
par ───┘ └─┘ ┴ └─┘ └┘ └─┘ └──
pid ───┘ └─┘ ┴ └─┘ └┘ └─┘ └┘└
st ─────────────────────────────────────────────────────────────────────────────────────────────────
456 | ._, ._, ⟨x, y, or.inr $ or.inl rfl⟩, ⟨z, w, or.inr $ or.inl rfl⟩, ha, hb :=
id └────┘ └────┘ └─┘
src ─┘ └────┘ └────┘ └─┘
typ ─┘ └────┘ └────┘ └─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
457 by rw [calc (⟨x, -y⟩ * ⟨z, -w⟩ : ℤ√d) = ⟨_, _⟩ : rfl
id └─┘
src └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘└─┘└
typ └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘└─┘└
doc └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
txt └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
par └──┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
pid └┘ ┴ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ └──────┘ └
st └──────────────────────────────────────────────────
458 ... = ⟨x * z + d * y * w, -(x * w + y * z)⟩ : by simp]; exact
id ┴ ┴ ┴ ┴ ┴
src ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴└──┘┴ └─────
typ ───────────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ └┘ ┴┴ ┴┴┴ ┴┴┴ ┴┴└───┘ ┴└──┘┴ └─────
doc ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴└──┘┴ └─────
txt ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴└──┘┴ └─────
par ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴└──┘┴ └─────
pid ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └────┘ └
st ───────────────────────────────────────────────────────┘└───┘┴└───────
459 nonnegg_pos_neg.2 (sq_le_mul.right.right.right (nonnegg_pos_neg.1 ha) (nonnegg_pos_neg.1 hb))
id └─────────────────────────┘ └┘ └─────────────┘ └┘
src ───┘ └─┘ └─────────────────────────┘┴ └─┘ └┘ └─────────────┘└─┘ └──
typ ───┘ └─┘ └─────────────────────────┘┴ └─┘└┘└┘ └─────────────┘└─┘└┘└──
doc ───┘ └─┘ ┴ └─┘ └┘ └─┘ └──
txt ───┘ └─┘ ┴ └─┘ └┘ └─┘ └──
par ───┘ └─┘ ┴ └─┘ └┘ └─┘ └──
pid ───┘ └─┘ ┴ └─┘ └┘ └─┘ └┘└
st ──────────────────────────────────────────────────────────────────────────────────────────────────
460 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
461
462 protected theorem mul_nonneg (a b : ℤ√d) : 0 ≤ a → 0 ≤ b → 0 ≤ a * b :=
id └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ ┴ ┴
typ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
463 by repeat {rw ← nonneg_iff_zero_le}; exact nonneg_mul
id └────────────────┘ └────────┘
src └──────┘└───┘└────────────────┘┴ └────┘└────────┘└
typ └──────┘└───┘└────────────────┘┴ └────┘└────────┘└
doc └──────┘└───┘ ┴ └────┘ └
txt └──────┘└───┘ ┴ └────┘ └
par └──────┘└───┘ ┴ └────┘ └
pid └─────┘ ┴ ┴ └
st └──────────────────────────────┘└┘└─────────────────
464
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
465 theorem not_sq_le_succ (c d y) (h : 0 < c) : ¬sq_le (y + 1) c 0 d :=
id ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴
src ─┘ ┴ ┴└───┘ ┴
typ ─┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴
doc ─┘ └───┘
txt ─┘
par ─┘
pid ─┘
st ─┘
466 not_le_of_gt $ mul_pos (mul_pos h $ nat.succ_pos _) $ nat.succ_pos _
id └──────────┘ └─────┘ └─────┘ ┴ └──────────┘ └──────────┘
src └──────────┘ └─────┘ └─────┘ └──────────┘ └──────────┘
typ └──────────┘ └─────┘ └─────┘ ┴ └──────────┘ └──────────┘
467
468 /-- A nonsquare is a natural number that is not equal to the square of an
469 integer. This is implemented as a typeclass because it's a necessary condition
470 for much of the Pell equation theory. -/
471 class nonsquare (x : ℕ) : Prop := (ns : ∀n : ℕ, x ≠ n*n)
id ┴ ┴ ┴ ┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴┴
472
473 parameter [dnsq : nonsquare d]
id └───────┘
src └───────┘
typ └───────┘
doc └───────┘
474 include dnsq
475
476 theorem d_pos : 0 < d := lt_of_le_of_ne (nat.zero_le _) $ ne.symm $ (nonsquare.ns d 0)
id ┴ ┴ └────────────┘ └─────────┘ └─────┘ └──────────┘ ┴
src ┴ └────────────┘ └─────────┘ └─────┘ └──────────┘
typ ┴ ┴ └────────────┘ └─────────┘ └─────┘ └──────────┘ ┴
477
478 theorem divides_sq_eq_zero {x y} (h : x * x = d * y * y) : x = 0 ∧ y = 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
479 let g := x.gcd y in or.elim g.eq_zero_or_pos
id ┴ ┴└──┘ ┴ └─────┘ ┴└─────────────┘
src └──┘ └─────┘ └─────────────┘
typ ┴ ┴└──┘ ┴ └─────┘ ┴└─────────────┘
480 (λH, ⟨nat.eq_zero_of_gcd_eq_zero_left H, nat.eq_zero_of_gcd_eq_zero_right H⟩)
id ┴ └─────────────────────────────┘ ┴ └──────────────────────────────┘ ┴
src └─────────────────────────────┘ └──────────────────────────────┘
typ ┴ └─────────────────────────────┘ ┴ └──────────────────────────────┘ ┴
481 (λgpos, false.elim $
id └──┘ └────────┘
src └────────┘
typ └──┘ └────────┘
482 let ⟨m, n, co, (hx : x = m * g), (hy : y = n * g)⟩ := nat.exists_coprime gpos in
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────┘ └──┘
src ┴ ┴ ┴ ┴ └────────────────┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────┘ └──┘
483 begin
st └─────
484 rw [hx, hy] at h,
id └┘ └┘
src └──┘ └┘ └────┘
typ └──┘└┘└┘└┘└────┘
doc └──┘ └┘ └────┘
txt └──┘ └┘ └────┘
par └──┘ └┘ └────┘
pid └┘ └┘ ┴└───┘
st ─────────────┘└──┘┴└───┘└─
485 have : m * m = d * (n * n) := nat.eq_of_mul_eq_mul_left (mul_pos gpos gpos)
id ┴ ┴ ┴ ┴ ┴ └───────────────────────┘ └─────┘ └──┘
src └─────┘ ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ └───┘└───────────────────────┘┴ └─────┘┴ ┴ └─
typ └─────┘ ┴┴┴┴┴┴┴┴┴ ┴ ┴ ┴┴└───┘└───────────────────────┘┴ └─────┘┴ ┴└──┘└─
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ └─
st ────────────────────────────────────────────────────────────────────────────────────
486 (by simpa [mul_comm, mul_left_comm] using h),
id └──────┘ └───────────┘ ┴
src ─────────┘ ┴└─────┘└──────┘└┘└───────────┘└──────┘ ┴
typ ─────────┘ ┴└─────┘└──────┘└┘└───────────┘└──────┘┴┴
doc ─────────┘ ┴└─────┘ └┘ └──────┘ ┴
txt ─────────┘ ┴└─────┘ └┘ └──────┘ ┴
par ─────────┘ ┴└─────┘ └┘ └──────┘ ┴
pid ─────────┘ └──────┘ └┘ └──────┘ ┴
st ────────────┘└──────────────────────────────────────┘┴└─
487 have co2 := let co1 := co.mul_right co in co1.mul co1,
id └──────────┘ └┘ └──┘
src └──────────┘ └──────┘└──────────┘┴ └──┘ └──┘┴
typ └──────────┘ └──────┘└──────────┘┴└┘└──┘ └──┘┴
doc └──────────┘ └──────┘ ┴ └──┘ ┴
txt └──────────┘ └──────┘ ┴ └──┘ ┴
par └──────────┘ └──────┘ ┴ └──┘ ┴
pid └──────┘┴└─┘ └──────┘ ┴ └──┘ ┴
st ────────────────────────────────────────────────────────────┘└─
488 exact nonsquare.ns d m (nat.dvd_antisymm (by rw this; apply dvd_mul_right) $
id └──────────┘ ┴ ┴ └──────────────┘ └──┘ └───────────┘
src └────┘└──────────┘┴ ┴ ┴ └──────────────┘┴ ┴└─┘ └┘└────┘└───────────┘└┘ └
typ └────┘└──────────┘┴┴┴┴┴ └──────────────┘┴ ┴└─┘└──┘└──────┘└───────────┘└┘ └
doc └────┘ ┴ ┴ ┴ ┴ ┴└─┘ └┘└────┘ └┘ └
txt └────┘ ┴ ┴ ┴ ┴ ┴└─┘ └┘└────┘ └┘ └
par └────┘ ┴ ┴ ┴ ┴ ┴└─┘ └──────┘ └┘ └
pid ┴ ┴ ┴ ┴ ┴ └──┘ └──────┘ └┘ └
st ───────────────────────────────────────────────────┘└───────────────────────────┘└───
489 co2.dvd_of_dvd_mul_right $ by simp [this])
id └──────────────────────┘ └──┘
src ─────────┘└──────────────────────┘┴ ┴ ┴└────┘ ┴└─
typ ─────────┘└──────────────────────┘┴ ┴ ┴└────┘└──┘┴└─
doc ─────────┘ ┴ ┴ ┴└────┘ ┴└─
txt ─────────┘ ┴ ┴ ┴└────┘ ┴└─
par ─────────┘ ┴ ┴ ┴└────┘ ┴└─
pid ─────────┘ ┴ ┴ └─────┘ └┘└
st ──────────────────────────────────────┘└──────────┘└─
490 end)
src ─────┘
typ ─────┘
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘└─┘
491
492 theorem divides_sq_eq_zero_z {x y : ℤ} (h : x * x = d * y * y) : x = 0 ∧ y = 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
493 by rw [mul_assoc, ← int.nat_abs_mul_self, ← int.nat_abs_mul_self, ← int.coe_nat_mul, ← mul_assoc] at h;
id └───────┘ └──────────────────┘ └──────────────────┘ └─────────────┘ └───────┘
src └──┘└───────┘└──┘└──────────────────┘└──┘└──────────────────┘└──┘└─────────────┘└──┘└───────┘└────┘
typ └──┘└───────┘└──┘└──────────────────┘└──┘└──────────────────┘└──┘└─────────────┘└──┘└───────┘└────┘
doc └──┘ └──┘ └──┘ └──┘ └──┘ └────┘
txt └──┘ └──┘ └──┘ └──┘ └──┘ └────┘
par └──┘ └──┘ └──┘ └──┘ └──┘ └────┘
pid └┘ └──┘ └──┘ └──┘ └──┘ ┴└───┘
st └────────────┘└──────────────────────┘└──────────────────────┘└─────────────────┘└───────────┘┴└──────
494 exact let ⟨h1, h2⟩ := divides_sq_eq_zero (int.coe_nat_inj h) in
id └┘ └┘ └────────────────┘ └─────────────┘ ┴
src └────┘ ┴ └┘ └───┘└────────────────┘┴ └─────────────┘┴ └────
typ └────┘ ┴ └┘└┘└┘└───┘└────────────────┘┴ └─────────────┘┴┴└────
doc └────┘ ┴ └┘ └───┘ ┴ ┴ └────
txt └────┘ ┴ └┘ └───┘ ┴ ┴ └────
par └────┘ ┴ └┘ └───┘ ┴ ┴ └────
pid ┴ ┴ └┘ └───┘ ┴ ┴ └────
st ──────────────────────────────────────────────────────────────────
495 ⟨int.eq_zero_of_nat_abs_eq_zero h1, int.eq_zero_of_nat_abs_eq_zero h2⟩
id └────────────────────────────┘
src ─┘ ┴ └┘└────────────────────────────┘┴ └─
typ ─┘ ┴ └┘└────────────────────────────┘┴ └─
doc ─┘ ┴ └┘ ┴ └─
txt ─┘ ┴ └┘ ┴ └─
par ─┘ ┴ └┘ ┴ └─
pid ─┘ ┴ └┘ ┴ ┴└
st ─────────────────────────────────────────────────────────────────────────
496
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
497 theorem not_divides_square (x y) : (x + 1) * (x + 1) ≠ d * (y + 1) * (y + 1) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
498 λe, by have t := (divides_sq_eq_zero e).left; contradiction
id ┴ └────────────────┘ ┴
src └────────┘ └────────────────┘┴ └────┘ └─────────────
typ ┴ └────────┘ └────────────────┘┴┴└────┘ └─────────────
doc └────────┘ ┴ └────┘ └─────────────
txt └────────┘ ┴ └────┘ └─────────────
par └────────┘ ┴ └────┘ └─────────────
pid └────┘┴└─┘ ┴ └───┘┴ └
st └─────────────────────────────────────────────────────
499
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
500 theorem nonneg_antisymm : Π {a : ℤ√d}, nonneg a → nonneg (-a) → a = 0
id ┴ └┘┴ └────┘ ┴ └────┘ ┴┴ ┴ ┴
src ─┘ └┘ └────┘ └────┘ ┴ ┴
typ ─┘ ┴ └┘┴ └────┘ ┴ └────┘ ┴┴ ┴ ┴
doc ─┘ └┘ └────┘ └────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
501 | ⟨0, 0⟩ xy yx := rfl
id └─┘
src └─┘
typ └─┘
502 | ⟨-[1+ x], -[1+ y]⟩ xy yx := false.elim xy
id └──┘ ┴ └──┘ ┴ └┘ └────────┘
src └──┘ ┴ └──┘ ┴ └────────┘
typ └──┘ ┴ └──┘ ┴ └┘ └────────┘
503 | ⟨(x+1:nat), (y+1:nat)⟩ xy yx := false.elim yx
id ┴ └─┘ ┴ └─┘ └┘ └────────┘
src ┴ └─┘ ┴ └─┘ └────────┘
typ ┴ └─┘ ┴ └─┘ └┘ └────────┘
504 | ⟨-[1+ x], 0⟩ xy yx := absurd xy (not_sq_le_succ _ _ _ dec_trivial)
id └──┘ ┴ └┘ └────┘ └────────────┘ └─────────┘
src └──┘ ┴ └────┘ └────────────┘ └─────────┘
typ └──┘ ┴ └┘ └────┘ └────────────┘ └─────────┘
doc └─────────┘
505 | ⟨(x+1:nat), 0⟩ xy yx := absurd yx (not_sq_le_succ _ _ _ dec_trivial)
id ┴ └─┘ └┘ └────┘ └────────────┘ └─────────┘
src ┴ └─┘ └────┘ └────────────┘ └─────────┘
typ ┴ └─┘ └┘ └────┘ └────────────┘ └─────────┘
doc └─────────┘
506 | ⟨0, -[1+ y]⟩ xy yx := absurd xy (not_sq_le_succ _ _ _ d_pos)
id └──┘ ┴ └┘ └────┘ └────────────┘ └───┘
src └──┘ ┴ └────┘ └────────────┘ └───┘
typ └──┘ ┴ └┘ └────┘ └────────────┘ └───┘
507 | ⟨0, (y+1:nat)⟩ _ yx := absurd yx (not_sq_le_succ _ _ _ d_pos)
id ┴ └─┘ └┘ └────┘ └────────────┘ └───┘
src ┴ └─┘ └────┘ └────────────┘ └───┘
typ ┴ └─┘ └┘ └────┘ └────────────┘ └───┘
508 | ⟨(x+1:nat), -[1+ y]⟩ (xy : sq_le _ _ _ _) (yx : sq_le _ _ _ _) :=
id ┴ └─┘ └──┘ ┴ ┴ └───┘ ┴ └───┘
src ┴ └─┘ └──┘ ┴ └───┘ └───┘
typ ┴ └─┘ └──┘ ┴ ┴ └───┘ ┴ └───┘
doc └───┘ └───┘
509 let t := le_antisymm yx xy in by rw[one_mul] at t; exact absurd t (not_divides_square _ _)
id ┴ └─────────┘ └─────┘ └────┘ ┴ └────────────────┘
src └─────────┘ └─┘└─────┘└────┘ └────┘└────┘┴ ┴ └────────────────┘└─────
typ ┴ └─────────┘ └─┘└─────┘└────┘ └────┘└────┘┴┴┴ └────────────────┘└─────
doc └─┘ └────┘ └────┘ ┴ ┴ └─────
txt └─┘ └────┘ └────┘ ┴ ┴ └─────
par └─┘ └────┘ └────┘ ┴ ┴ └─────
pid ┴ ┴└───┘ ┴ ┴ ┴ └───┘└
st └─────────┘┴└──────────────────────────────────────────────
510 | ⟨-[1+ x], (y+1:nat)⟩ (xy : sq_le _ _ _ _) (yx : sq_le _ _ _ _) :=
id └──┘ ┴ ┴ └─┘ ┴ └───┘ ┴ └───┘
src ─┘ └──┘ ┴ ┴ └─┘ └───┘ └───┘
typ ─┘ └──┘ ┴ ┴ └─┘ ┴ └───┘ ┴ └───┘
doc ─┘ └───┘ └───┘
txt ─┘
par ─┘
pid ─┘
st ─┘
511 let t := le_antisymm xy yx in by rw[one_mul] at t; exact absurd t (not_divides_square _ _)
id ┴ └─────────┘ └─────┘ └────┘ ┴ └────────────────┘
src └─────────┘ └─┘└─────┘└────┘ └────┘└────┘┴ ┴ └────────────────┘└─────
typ ┴ └─────────┘ └─┘└─────┘└────┘ └────┘└────┘┴┴┴ └────────────────┘└─────
doc └─┘ └────┘ └────┘ ┴ ┴ └─────
txt └─┘ └────┘ └────┘ ┴ ┴ └─────
par └─┘ └────┘ └────┘ ┴ ┴ └─────
pid ┴ ┴└───┘ ┴ ┴ ┴ └───┘└
st └─────────┘┴└──────────────────────────────────────────────
512
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
513 theorem le_antisymm {a b : ℤ√d} (ab : a ≤ b) (ba : b ≤ a) : a = b :=
id └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ─┘ └┘ ┴ ┴ ┴
typ ─┘ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ─┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
514 eq_of_sub_eq_zero $ nonneg_antisymm ba (by rw neg_sub; exact ab)
id └───────────────┘ └─────────────┘ └┘ └─────┘ └┘
src └───────────────┘ └─────────────┘ └─┘└─────┘ └────┘
typ └───────────────┘ └─────────────┘ └┘ └─┘└─────┘ └────┘└┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └───────────────────┘
515
516 instance : decidable_linear_order ℤ√d :=
id └────────────────────┘ └┘┴
src └────────────────────┘ └┘
typ └────────────────────┘ └┘┴
doc └┘
517 { le_antisymm := @zsqrtd.le_antisymm,
id └────────────────┘
src └────────────────┘
typ └────────────────┘
518 le_total := zsqrtd.le_total,
id └─────────────┘
src └─────────────┘
typ └─────────────┘
519 decidable_le := zsqrtd.decidable_le,
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
520 ..zsqrtd.preorder }
id └─────────────┘
src └─────────────┘
typ └─────────────┘
521
522 protected theorem eq_zero_or_eq_zero_of_mul_eq_zero : Π {a b : ℤ√d}, a * b = 0 → a = 0 ∨ b = 0
id ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └┘┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
523 | ⟨x, y⟩ ⟨z, w⟩ h := by injection h with h1 h2; exact
id ┴
src └────────┘ └─────────┘ └─────
typ └────────┘┴└─────────┘ └─────
doc └────────┘ └─────────┘ └─────
txt └────────┘ └─────────┘ └─────
par └────────┘ └─────────┘ └─────
pid ┴ └─────────┘ └
st └──────────────────────────────
524 have h1 : x*z = -(d*y*w), from eq_neg_of_add_eq_zero h1,
id ┴ ┴ ┴ └───────────────────┘ └┘
src ───┘ └────┘ ┴ ┴┴┴┴ └──────┘└───────────────────┘┴ └─
typ ───┘ └────┘ ┴ ┴┴┴┴ └──────┘└───────────────────┘┴└┘└─
doc ───┘ └────┘ ┴ ┴ └──────┘ ┴ └─
txt ───┘ └────┘ ┴ ┴ └──────┘ ┴ └─
par ───┘ └────┘ ┴ ┴ └──────┘ ┴ └─
pid ───┘ └────┘ ┴ ┴ └──────┘ ┴ └─
st ─────────────────────────────────────────────────────────────
525 have h2 : x*w = -(y*z), from eq_neg_of_add_eq_zero h2,
id └┘
src ───┘ └────┘ ┴ ┴ └──────┘ ┴ └─
typ ───┘ └────┘ ┴ ┴ └──────┘ ┴└┘└─
doc ───┘ └────┘ ┴ ┴ └──────┘ ┴ └─
txt ───┘ └────┘ ┴ ┴ └──────┘ ┴ └─
par ───┘ └────┘ ┴ ┴ └──────┘ ┴ └─
pid ───┘ └────┘ ┴ ┴ └──────┘ ┴ └─
st ───────────────────────────────────────────────────────────
526 have fin : x*x = d*y*y → (⟨x, y⟩:ℤ√d) = 0, from
id ┴
src ───┘ └─────┘ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └────────
typ ───┘ └─────┘ ┴┴┴ ┴ ┴ └┘ └┘ └┘ └────────
doc ───┘ └─────┘ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └────────
txt ───┘ └─────┘ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └────────
par ───┘ └─────┘ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └────────
pid ───┘ └─────┘ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └────────
st ────────────────────────────────────────────────────
527 λe, match x, y, divides_sq_eq_zero_z e with ._, ._, ⟨rfl, rfl⟩ := rfl end,
id ┴ ┴ └──────────────────┘ └─┘
src ───┘ └─┘ ┴ └┘ └┘└──────────────────┘┴ └────┘ └┘ └┘ └┘ └───┘└─┘└─────
typ ───┘ └─┘ ┴┴└┘┴└┘└──────────────────┘┴ └────┘ └┘ └┘ └┘ └───┘└─┘└─────
doc ───┘ └─┘ ┴ └┘ └┘ ┴ └────┘ └┘ └┘ └┘ └───┘ └─────
txt ───┘ └─┘ ┴ └┘ └┘ ┴ └────┘ └┘ └┘ └┘ └───┘ └─────
par ───┘ └─┘ ┴ └┘ └┘ ┴ └────┘ └┘ └┘ └┘ └───┘ └─────
pid ───┘ └─┘ ┴ └┘ └┘ ┴ └────┘ └┘ └┘ └┘ └───┘ └─────
st ───────────────────────────────────────────────────────────────────────────────
528 if z0 : z = 0 then if w0 : w = 0 then
id └┘ ┴ ┴
src ───┘└┘└────┘ ┴ └──────┘ └────┘ ┴ └───────
typ ───┘└┘└────┘ ┴┴└──────┘ └────┘ ┴┴└───────
doc ───┘ └────┘ ┴ └──────┘ └────┘ ┴ └───────
txt ───┘ └────┘ ┴ └──────┘ └────┘ ┴ └───────
par ───┘ └────┘ ┴ └──────┘ └────┘ ┴ └───────
pid ───┘ └────┘ ┴ └──────┘ └────┘ ┴ └───────
st ──────────────────────────────────────────
529 or.inr (match z, w, z0, w0 with ._, ._, rfl, rfl := rfl end)
id └────┘
src ─────┘└────┘┴ ┴ └┘ └┘ └┘ └────┘ └┘ └┘ └┘ └──┘ └─────
typ ─────┘└────┘┴ ┴ └┘ └┘ └┘ └────┘ └┘ └┘ └┘ └──┘ └─────
doc ─────┘ ┴ ┴ └┘ └┘ └┘ └────┘ └┘ └┘ └┘ └──┘ └─────
txt ─────┘ ┴ ┴ └┘ └┘ └┘ └────┘ └┘ └┘ └┘ └──┘ └─────
par ─────┘ ┴ ┴ └┘ └┘ └┘ └────┘ └┘ └┘ └┘ └──┘ └─────
pid ─────┘ ┴ ┴ └┘ └┘ └┘ └────┘ └┘ └┘ └┘ └──┘ └─────
st ───────────────────────────────────────────────────────────────────
530 else
src ─────────
typ ─────────
doc ─────────
txt ─────────
par ─────────
pid ─────────
st ─────────
531 or.inl $ fin $ eq_of_mul_eq_mul_right w0 $ calc
id ┴
src ──────┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴ └
typ ──────┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴ └
doc ──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
txt ──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
par ──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
pid ──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
st ───────────────────────────────────────────────────────
532 x * x * w = -y * (x * z) : by simp [h2, mul_assoc, mul_left_comm]
id └┘ └───────┘ └───────────┘
src ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└────┘ └┘└───────┘└┘└───────────┘└─
typ ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└────┘└┘└┘└───────┘└┘└───────────┘└─
doc ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└────┘ └┘ └┘ └─
txt ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└────┘ └┘ └┘ └─
par ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└────┘ └┘ └┘ └─
pid ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘ └┘ └┘ └─
st ─────────────────────────────────────┘└────────────────────────────────────
533 ... = d * y * y * w : by simp [h1, mul_assoc, mul_left_comm]
id └┘ └───────┘ └───────────┘
src ──────────────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘ └┘└───────┘└┘└───────────┘└─
typ ──────────────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘└┘└┘└───────┘└┘└───────────┘└─
doc ──────────────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘ └┘ └┘ └─
txt ──────────────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘ └┘ └┘ └─
par ──────────────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘ └┘ └┘ └─
pid ──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─────┘ └┘ └┘ └─
st ──────────────┘└──────────────────────┘└────────────────────────────────────
534 else
src ───┘└────
typ ───┘└────
doc ───┘└────
txt ───┘└────
par ───┘└────
pid ─────────
st ───┘└────
535 or.inl $ fin $ eq_of_mul_eq_mul_right z0 $ calc
id └────┘ ┴ └────────────────────┘
src ──────┘└────┘┴ ┴ ┴ ┴└────────────────────┘┴ ┴ ┴ └
typ ──────┘└────┘┴┴┴ ┴ ┴└────────────────────┘┴ ┴ ┴ └
doc ──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
txt ──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
par ──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
pid ──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
st ───────────────────────────────────────────────────────
536 x * x * z = d * -y * (x * w) : by simp [h1, mul_assoc, mul_left_comm]
id ┴ └┘ └───────┘ └───────────┘
src ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└────┘ └┘└───────┘└┘└───────────┘└─
typ ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴└──┘ ┴└────┘└┘└┘└───────┘└┘└───────────┘└─
doc ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└────┘ └┘ └┘ └─
txt ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└────┘ └┘ └┘ └─
par ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└────┘ └┘ └┘ └─
pid ────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘ └┘ └┘ └─
st ─────────────────────────────────────────┘└────────────────────────────────────
537 ... = d * y * y * z : by simp [h2, mul_assoc, mul_left_comm]
id ┴ ┴ └┘ └───────┘ └───────────┘
src ──────────────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘ └┘└───────┘└┘└───────────┘└─
typ ──────────────┘└──┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴└─┘ ┴└────┘└┘└┘└───────┘└┘└───────────┘└─
doc ──────────────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘ └┘ └┘ └─
txt ──────────────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘ └┘ └┘ └─
par ──────────────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘ └┘ └┘ └─
pid ──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─────┘ └┘ └┘ └─
st ──────────────┘└──────────────────────┘└────────────────────────────────────
538
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
539 instance : integral_domain ℤ√d :=
id └─────────────┘ └┘┴
src ─┘ └─────────────┘ └┘
typ ─┘ └─────────────┘ └┘┴
doc ─┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
540 { zero_ne_one := zero_ne_one,
id └─────────┘
src └─────────┘
typ └─────────┘
541 eq_zero_or_eq_zero_of_mul_eq_zero := @zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero,
id └──────────────────────────────────────┘
src └──────────────────────────────────────┘
typ └──────────────────────────────────────┘
542 ..zsqrtd.comm_ring }
id └──────────────┘
src └──────────────┘
typ └──────────────┘
543
544 protected theorem mul_pos (a b : ℤ√d) (a0 : 0 < a) (b0 : 0 < b) : 0 < a * b := λab,
id └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src └┘ ┴ ┴ ┴ ┴
typ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
doc └┘
545 or.elim (eq_zero_or_eq_zero_of_mul_eq_zero (le_antisymm ab (mul_nonneg _ _ (le_of_lt a0) (le_of_lt b0))))
id └─────┘ └───────────────────────────────┘ └─────────┘ └┘ └────────┘ └──────┘ └┘ └──────┘ └┘
src └─────┘ └───────────────────────────────┘ └─────────┘ └────────┘ └──────┘ └──────┘
typ └─────┘ └───────────────────────────────┘ └─────────┘ └┘ └────────┘ └──────┘ └┘ └──────┘ └┘
546 (λe, ne_of_gt a0 e)
id ┴ └──────┘ └┘ ┴
src └──────┘
typ ┴ └──────┘ └┘ ┴
547 (λe, ne_of_gt b0 e)
id ┴ └──────┘ └┘ ┴
src └──────┘
typ ┴ └──────┘ └┘ ┴
548
549 instance : decidable_linear_ordered_comm_ring ℤ√d :=
id └────────────────────────────────┘ └┘┴
src └────────────────────────────────┘ └┘
typ └────────────────────────────────┘ └┘┴
doc └┘
550 { add_le_add_left := @zsqrtd.add_le_add_left,
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
551 add_lt_add_left := @zsqrtd.add_lt_add_left,
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
552 zero_ne_one := zero_ne_one,
id └─────────┘
src └─────────┘
typ └─────────┘
553 mul_nonneg := @zsqrtd.mul_nonneg,
id └───────────────┘
src └───────────────┘
typ └───────────────┘
554 mul_pos := @zsqrtd.mul_pos,
id └────────────┘
src └────────────┘
typ └────────────┘
555 zero_lt_one := dec_trivial,
id └─────────┘
src └─────────┘
typ └─────────┘
doc └─────────┘
556 ..zsqrtd.comm_ring, ..zsqrtd.decidable_linear_order }
id └──────────────┘ └───────────────────────────┘
src └──────────────┘ └───────────────────────────┘
typ └──────────────┘ └───────────────────────────┘
557
558 instance : decidable_linear_ordered_semiring ℤ√d := by apply_instance
id └───────────────────────────────┘ └┘┴
src └───────────────────────────────┘ └┘ └──────────────
typ └───────────────────────────────┘ └┘┴ └──────────────
doc └┘ └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
559 instance : linear_ordered_semiring ℤ√d := by apply_instance
id └─────────────────────┘ └┘┴
src ─┘ └─────────────────────┘ └┘ └──────────────
typ ─┘ └─────────────────────┘ └┘┴ └──────────────
doc ─┘ └┘ └──────────────
txt ─┘ └──────────────
par ─┘ └──────────────
pid ─┘ └
st ─┘ └───────────────
560 instance : ordered_semiring ℤ√d := by apply_instance
id └──────────────┘ └┘┴
src ─┘ └──────────────┘ └┘ └──────────────
typ ─┘ └──────────────┘ └┘┴ └──────────────
doc ─┘ └┘ └──────────────
txt ─┘ └──────────────
par ─┘ └──────────────
pid ─┘ └
st ─┘ └───────────────
561
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
562 end
563 end zsqrtd